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 27948
Description: Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2370. 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 27947. (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 27943 . . 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 620 . 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 2574 . . . . 5  |-  F/_ x B
4 nfreu1 2880 . . . . 5  |-  F/ x E! x  e.  A  ph
53, 4nfreu 2884 . . . 4  |-  F/ x E! y  e.  B  E! x  e.  A  ph
65reuan 27936 . . 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 439 . . . . . 6  |-  ( ( E! x  e.  A  ph 
/\  E. y  e.  B  ph )  <->  ( E. y  e.  B  ph  /\  E! x  e.  A  ph )
)
87reubii 2896 . . . . 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 2764 . . . . . 6  |-  F/ y E. y  e.  B  ph
109reuan 27936 . . . . 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 439 . . . . 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 264 . . . 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 2896 . . 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 439 . . 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 271 . 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 27947 . 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 269 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 set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wrex 2708   E!wreu 2709
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715
  Copyright terms: Public domain W3C validator