Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2reu8 Structured version   Unicode version

Theorem 2reu8 38484
Description: Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2359. Curiously, we can put  E! on either of the internal conjuncts but not both. We can also commute  E! x  e.  A E! y  e.  B using 2reu7 38483. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
Assertion
Ref Expression
2reu8  |-  ( E! x  e.  A  E! y  e.  B  ( E. x  e.  A  ph 
/\  E. y  e.  B  ph )  <->  E! x  e.  A  E! y  e.  B  ( E! x  e.  A  ph 
/\  E. y  e.  B  ph ) )
Distinct variable groups:    x, y, A    x, B, y
Allowed substitution hints:    ph( x, y)

Proof of Theorem 2reu8
StepHypRef Expression
1 2reu2 38479 . . 3  |-  ( E! x  e.  A  E. y  e.  B  ph  ->  ( E! y  e.  B  E! x  e.  A  ph  <->  E! y  e.  B  E. x  e.  A  ph )
)
21pm5.32i 641 . 2  |-  ( ( E! x  e.  A  E. y  e.  B  ph 
/\  E! y  e.  B  E! x  e.  A  ph )  <->  ( E! x  e.  A  E. y  e.  B  ph  /\  E! y  e.  B  E. x  e.  A  ph ) )
3 nfcv 2580 . . . . 5  |-  F/_ x B
4 nfreu1 2996 . . . . 5  |-  F/ x E! x  e.  A  ph
53, 4nfreu 3000 . . . 4  |-  F/ x E! y  e.  B  E! x  e.  A  ph
65reuan 38472 . . 3  |-  ( E! x  e.  A  ( E! y  e.  B  E! x  e.  A  ph 
/\  E. y  e.  B  ph )  <->  ( E! y  e.  B  E! x  e.  A  ph  /\  E! x  e.  A  E. y  e.  B  ph )
)
7 ancom 451 . . . . . 6  |-  ( ( E! x  e.  A  ph 
/\  E. y  e.  B  ph )  <->  ( E. y  e.  B  ph  /\  E! x  e.  A  ph )
)
87reubii 3012 . . . . 5  |-  ( E! y  e.  B  ( E! x  e.  A  ph 
/\  E. y  e.  B  ph )  <->  E! y  e.  B  ( E. y  e.  B  ph 
/\  E! x  e.  A  ph ) )
9 nfre1 2883 . . . . . 6  |-  F/ y E. y  e.  B  ph
109reuan 38472 . . . . 5  |-  ( E! y  e.  B  ( E. y  e.  B  ph 
/\  E! x  e.  A  ph )  <->  ( E. y  e.  B  ph  /\  E! y  e.  B  E! x  e.  A  ph ) )
11 ancom 451 . . . . 5  |-  ( ( E. y  e.  B  ph 
/\  E! y  e.  B  E! x  e.  A  ph )  <->  ( E! y  e.  B  E! x  e.  A  ph  /\  E. y  e.  B  ph ) )
128, 10, 113bitri 274 . . . 4  |-  ( E! y  e.  B  ( E! x  e.  A  ph 
/\  E. y  e.  B  ph )  <->  ( E! y  e.  B  E! x  e.  A  ph  /\  E. y  e.  B  ph )
)
1312reubii 3012 . . 3  |-  ( E! x  e.  A  E! y  e.  B  ( E! x  e.  A  ph 
/\  E. y  e.  B  ph )  <->  E! x  e.  A  ( E! y  e.  B  E! x  e.  A  ph 
/\  E. y  e.  B  ph ) )
14 ancom 451 . . 3  |-  ( ( E! x  e.  A  E. y  e.  B  ph 
/\  E! y  e.  B  E! x  e.  A  ph )  <->  ( E! y  e.  B  E! x  e.  A  ph  /\  E! x  e.  A  E. y  e.  B  ph ) )
156, 13, 143bitr4ri 281 . 2  |-  ( ( E! x  e.  A  E. y  e.  B  ph 
/\  E! y  e.  B  E! x  e.  A  ph )  <->  E! x  e.  A  E! y  e.  B  ( E! x  e.  A  ph  /\  E. y  e.  B  ph ) )
16 2reu7 38483 . 2  |-  ( ( E! x  e.  A  E. y  e.  B  ph 
/\  E! y  e.  B  E. x  e.  A  ph )  <->  E! x  e.  A  E! y  e.  B  ( E. x  e.  A  ph  /\  E. y  e.  B  ph ) )
172, 15, 163bitr3ri 279 1  |-  ( E! x  e.  A  E! y  e.  B  ( E. x  e.  A  ph 
/\  E. y  e.  B  ph )  <->  E! x  e.  A  E! y  e.  B  ( E! x  e.  A  ph 
/\  E. y  e.  B  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370   E.wrex 2772   E!wreu 2773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator