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

This theorem relates to wl-mo3t 31863, 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 2174 and sbco 2207. So  E* x ph  <->  E* y [ y  /  x ] ph is provable from wl-mo3t 31863 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 31863 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 31839 . . 3  |-  ( A. x F/ y ph  ->  ( E. x ph  <->  E. y [ y  /  x ] ph ) )
2 wl-sb8eut 31864 . . 3  |-  ( A. x F/ y ph  ->  ( E! x ph  <->  E! y [ y  /  x ] ph ) )
31, 2imbi12d 322 . 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 2271 . 2  |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
5 df-mo 2271 . 2  |-  ( E* y [ y  /  x ] ph  <->  ( E. y [ y  /  x ] ph  ->  E! y [ y  /  x ] ph ) )
63, 4, 53bitr4g 292 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 188   A.wal 1436   E.wex 1660   F/wnf 1664   [wsb 1787   E!weu 2266   E*wmo 2267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator