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 31375
Description: Substitution of variable in universal quantifier. Closed form of sb8mo 2275.

This theorem relates to wl-mo3t 31373, 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 2144 and sbco 2178. So  E* x ph  <->  E* y [ y  /  x ] ph is provable from wl-mo3t 31373 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 31373 to be more fundamental, as it hints how the "at most one" objects on both sides of the biconditional 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 31353 . . 3  |-  ( A. x F/ y ph  ->  ( E. x ph  <->  E. y [ y  /  x ] ph ) )
2 wl-sb8eut 31374 . . 3  |-  ( A. x F/ y ph  ->  ( E! x ph  <->  E! y [ y  /  x ] ph ) )
31, 2imbi12d 318 . 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 2243 . 2  |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
5 df-mo 2243 . 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 1403   E.wex 1633   F/wnf 1637   [wsb 1763   E!weu 2238   E*wmo 2239
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator