Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-sb8mot Structured version   Unicode version

Theorem wl-sb8mot 28418
Description: Substitution of variable in universal quantifier. Closed form of sb8mo 2295.

This theorem relates to wl-mo3t 28416, since replacing  ph with  [ y  /  x ] ph in the latter yields subexpressions like  [ x  / 
y ] [ y  /  x ] ph, which can be reduced to  ph via sbft 2070 and sbco 2106. So  E* x ph  <->  E* y [ y  /  x ] ph is provable from wl-mo3t 28416 in a simple fashion, unfortunately only if  x and  y are known to be distinct. To avoid any hassle with distinctors, we prefer to derive this theorem independently, ignoring the close connection between both theorems. From an educational standpoint, one would assume wl-mo3t 28416 to be more fundamental, as it hints how the "at most one" objects on both sides of the bi-conditional correlate (they are the same), if they exist at all, and then prove this theorem from it. (Contributed by Wolf Lammen, 11-Aug-2019.)

Assertion
Ref Expression
wl-sb8mot  |-  ( A. x F/ y ph  ->  ( E* x ph  <->  E* y [ y  /  x ] ph ) )

Proof of Theorem wl-sb8mot
StepHypRef Expression
1 wl-sb8et 28396 . . 3  |-  ( A. x F/ y ph  ->  ( E. x ph  <->  E. y [ y  /  x ] ph ) )
2 wl-sb8eut 28417 . . 3  |-  ( A. x F/ y ph  ->  ( E! x ph  <->  E! y [ y  /  x ] ph ) )
31, 2imbi12d 320 . 2  |-  ( A. x F/ y ph  ->  ( ( E. x ph  ->  E! x ph )  <->  ( E. y [ y  /  x ] ph  ->  E! y [ y  /  x ] ph ) ) )
4 df-mo 2258 . 2  |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
5 df-mo 2258 . 2  |-  ( E* y [ y  /  x ] ph  <->  ( E. y [ y  /  x ] ph  ->  E! y [ y  /  x ] ph ) )
63, 4, 53bitr4g 288 1  |-  ( A. x F/ y ph  ->  ( E* x ph  <->  E* y [ y  /  x ] ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1367   E.wex 1586   F/wnf 1589   [wsb 1700   E!weu 2253   E*wmo 2254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator