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

Theorem 2reu8 27382
Description: Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2230. 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 27381. (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 27377 . . 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 618 . 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 2419 . . . . 5  |-  F/_ x B
4 nfreu1 2710 . . . . 5  |-  F/ x E! x  e.  A  ph
53, 4nfreu 2714 . . . 4  |-  F/ x E! y  e.  B  E! x  e.  A  ph
65reuan 27370 . . 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 437 . . . . . 6  |-  ( ( E! x  e.  A  ph 
/\  E. y  e.  B  ph )  <->  ( E. y  e.  B  ph  /\  E! x  e.  A  ph )
)
87reubii 2726 . . . . 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 2599 . . . . . 6  |-  F/ y E. y  e.  B  ph
109reuan 27370 . . . . 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 437 . . . . 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 262 . . . 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 2726 . . 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 437 . . 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 269 . 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 27381 . 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 267 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 176    /\ wa 358   E.wrex 2544   E!wreu 2545
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551
  Copyright terms: Public domain W3C validator