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

Theorem 2reu4a 28070
Description: Definition of double restricted existential uniqueness ("exactly one  x and exactly one  y"), analogous to 2eu4 2239 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 28071). (Contributed by Alexander van der Vekens, 1-Jul-2017.)
Assertion
Ref Expression
2reu4a  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  (
( 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. z  e.  A  E. w  e.  B  A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) ) )
Distinct variable groups:    z, w, ph    x, w, y, A, z   
w, B, x, y, z
Allowed substitution hints:    ph( x, y)

Proof of Theorem 2reu4a
StepHypRef Expression
1 reu3 2968 . . . 4  |-  ( E! x  e.  A  E. y  e.  B  ph  <->  ( E. x  e.  A  E. y  e.  B  ph  /\  E. z  e.  A  A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
) ) )
2 reu3 2968 . . . 4  |-  ( E! y  e.  B  E. x  e.  A  ph  <->  ( E. y  e.  B  E. x  e.  A  ph  /\  E. w  e.  B  A. y  e.  B  ( E. x  e.  A  ph 
->  y  =  w
) ) )
31, 2anbi12i 678 . . 3  |-  ( ( 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. z  e.  A  A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
) )  /\  ( E. y  e.  B  E. x  e.  A  ph 
/\  E. w  e.  B  A. y  e.  B  ( E. x  e.  A  ph 
->  y  =  w
) ) ) )
43a1i 10 . 2  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  (
( 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. z  e.  A  A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
) )  /\  ( E. y  e.  B  E. x  e.  A  ph 
/\  E. w  e.  B  A. y  e.  B  ( E. x  e.  A  ph 
->  y  =  w
) ) ) ) )
5 an4 797 . . 3  |-  ( ( ( E. x  e.  A  E. y  e.  B  ph  /\  E. z  e.  A  A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
) )  /\  ( E. y  e.  B  E. x  e.  A  ph 
/\  E. w  e.  B  A. y  e.  B  ( E. x  e.  A  ph 
->  y  =  w
) ) )  <->  ( ( E. x  e.  A  E. y  e.  B  ph 
/\  E. y  e.  B  E. x  e.  A  ph )  /\  ( E. z  e.  A  A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
)  /\  E. w  e.  B  A. y  e.  B  ( E. x  e.  A  ph  ->  y  =  w ) ) ) )
65a1i 10 . 2  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  (
( ( E. x  e.  A  E. y  e.  B  ph  /\  E. z  e.  A  A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
) )  /\  ( E. y  e.  B  E. x  e.  A  ph 
/\  E. w  e.  B  A. y  e.  B  ( E. x  e.  A  ph 
->  y  =  w
) ) )  <->  ( ( E. x  e.  A  E. y  e.  B  ph 
/\  E. y  e.  B  E. x  e.  A  ph )  /\  ( E. z  e.  A  A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
)  /\  E. w  e.  B  A. y  e.  B  ( E. x  e.  A  ph  ->  y  =  w ) ) ) ) )
7 rexcom 2714 . . . . . 6  |-  ( E. y  e.  B  E. x  e.  A  ph  <->  E. x  e.  A  E. y  e.  B  ph )
87anbi2i 675 . . . . 5  |-  ( ( 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. x  e.  A  E. y  e.  B  ph )
)
9 anidm 625 . . . . 5  |-  ( ( E. x  e.  A  E. y  e.  B  ph 
/\  E. x  e.  A  E. y  e.  B  ph )  <->  E. x  e.  A  E. y  e.  B  ph )
108, 9bitri 240 . . . 4  |-  ( ( 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 )
1110a1i 10 . . 3  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  (
( 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 )
)
12 r19.26 2688 . . . . . . . 8  |-  ( A. x  e.  A  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) )  <->  ( A. x  e.  A  A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) )
13 nfra1 2606 . . . . . . . . . . . . . 14  |-  F/ x A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w )
1413r19.3rz 3558 . . . . . . . . . . . . 13  |-  ( A  =/=  (/)  ->  ( A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w )  <->  A. x  e.  A  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) )
1514bicomd 192 . . . . . . . . . . . 12  |-  ( A  =/=  (/)  ->  ( A. x  e.  A  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w )  <->  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) )
1615adantr 451 . . . . . . . . . . 11  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A. x  e.  A  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w )  <->  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) )
1716adantr 451 . . . . . . . . . 10  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. x  e.  A  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w )  <->  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) )
1817anbi2d 684 . . . . . . . . 9  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( ( A. x  e.  A  A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) )  <->  ( A. x  e.  A  A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) ) )
19 jcab 833 . . . . . . . . . . . . . 14  |-  ( (
ph  ->  ( x  =  z  /\  y  =  w ) )  <->  ( ( ph  ->  x  =  z )  /\  ( ph  ->  y  =  w ) ) )
2019ralbii 2580 . . . . . . . . . . . . 13  |-  ( A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  A. y  e.  B  ( ( ph  ->  x  =  z )  /\  ( ph  ->  y  =  w ) ) )
21 r19.26 2688 . . . . . . . . . . . . 13  |-  ( A. y  e.  B  (
( ph  ->  x  =  z )  /\  ( ph  ->  y  =  w ) )  <->  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. y  e.  B  ( ph  ->  y  =  w ) ) )
2220, 21bitri 240 . . . . . . . . . . . 12  |-  ( A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. y  e.  B  ( ph  ->  y  =  w ) ) )
2322ralbii 2580 . . . . . . . . . . 11  |-  ( A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  A. x  e.  A  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. y  e.  B  ( ph  ->  y  =  w ) ) )
24 r19.26 2688 . . . . . . . . . . 11  |-  ( A. x  e.  A  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. y  e.  B  ( ph  ->  y  =  w ) )  <->  ( A. x  e.  A  A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) )
2523, 24bitri 240 . . . . . . . . . 10  |-  ( A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  ( A. x  e.  A  A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) )
2625a1i 10 . . . . . . . . 9  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  ( A. x  e.  A  A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) ) )
2718, 26bitr4d 247 . . . . . . . 8  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( ( A. x  e.  A  A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) )  <->  A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
2812, 27syl5rbb 249 . . . . . . 7  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  A. x  e.  A  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) ) )
29 r19.26 2688 . . . . . . . . 9  |-  ( A. y  e.  B  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  ( ph  ->  y  =  w ) )  <->  ( A. y  e.  B  A. y  e.  B  ( ph  ->  x  =  z )  /\  A. y  e.  B  A. x  e.  A  ( ph  ->  y  =  w ) ) )
30 nfra1 2606 . . . . . . . . . . . . 13  |-  F/ y A. y  e.  B  ( ph  ->  x  =  z )
3130r19.3rz 3558 . . . . . . . . . . . 12  |-  ( B  =/=  (/)  ->  ( A. y  e.  B  ( ph  ->  x  =  z )  <->  A. y  e.  B  A. y  e.  B  ( ph  ->  x  =  z ) ) )
3231ad2antlr 707 . . . . . . . . . . 11  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. y  e.  B  ( ph  ->  x  =  z )  <->  A. y  e.  B  A. y  e.  B  ( ph  ->  x  =  z ) ) )
3332bicomd 192 . . . . . . . . . 10  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. y  e.  B  A. y  e.  B  ( ph  ->  x  =  z )  <->  A. y  e.  B  ( ph  ->  x  =  z ) ) )
34 ralcom 2713 . . . . . . . . . . 11  |-  ( A. y  e.  B  A. x  e.  A  ( ph  ->  y  =  w )  <->  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) )
3534a1i 10 . . . . . . . . . 10  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. y  e.  B  A. x  e.  A  ( ph  ->  y  =  w )  <->  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) )
3633, 35anbi12d 691 . . . . . . . . 9  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( ( A. y  e.  B  A. y  e.  B  ( ph  ->  x  =  z )  /\  A. y  e.  B  A. x  e.  A  ( ph  ->  y  =  w ) )  <->  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) ) )
3729, 36syl5bb 248 . . . . . . . 8  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. y  e.  B  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  ( ph  ->  y  =  w ) )  <->  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) ) )
3837ralbidv 2576 . . . . . . 7  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. x  e.  A  A. y  e.  B  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  ( ph  ->  y  =  w ) )  <->  A. x  e.  A  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) ) ) )
3928, 38bitr4d 247 . . . . . 6  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  A. x  e.  A  A. y  e.  B  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  ( ph  ->  y  =  w ) ) ) )
40 r19.23v 2672 . . . . . . . . 9  |-  ( A. y  e.  B  ( ph  ->  x  =  z )  <->  ( E. y  e.  B  ph  ->  x  =  z ) )
41 r19.23v 2672 . . . . . . . . 9  |-  ( A. x  e.  A  ( ph  ->  y  =  w )  <->  ( E. x  e.  A  ph  ->  y  =  w ) )
4240, 41anbi12i 678 . . . . . . . 8  |-  ( ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  ( ph  ->  y  =  w ) )  <->  ( ( E. y  e.  B  ph 
->  x  =  z
)  /\  ( E. x  e.  A  ph  ->  y  =  w ) ) )
43422ralbii 2582 . . . . . . 7  |-  ( A. x  e.  A  A. y  e.  B  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  ( ph  ->  y  =  w ) )  <->  A. x  e.  A  A. y  e.  B  ( ( E. y  e.  B  ph 
->  x  =  z
)  /\  ( E. x  e.  A  ph  ->  y  =  w ) ) )
4443a1i 10 . . . . . 6  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. x  e.  A  A. y  e.  B  ( A. y  e.  B  ( ph  ->  x  =  z )  /\  A. x  e.  A  ( ph  ->  y  =  w ) )  <->  A. x  e.  A  A. y  e.  B  ( ( E. y  e.  B  ph 
->  x  =  z
)  /\  ( E. x  e.  A  ph  ->  y  =  w ) ) ) )
45 df-ne 2461 . . . . . . . . . . . 12  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
4645biimpi 186 . . . . . . . . . . 11  |-  ( A  =/=  (/)  ->  -.  A  =  (/) )
47 df-ne 2461 . . . . . . . . . . . 12  |-  ( B  =/=  (/)  <->  -.  B  =  (/) )
4847biimpi 186 . . . . . . . . . . 11  |-  ( B  =/=  (/)  ->  -.  B  =  (/) )
4946, 48anim12i 549 . . . . . . . . . 10  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( -.  A  =  (/)  /\  -.  B  =  (/) ) )
5049olcd 382 . . . . . . . . 9  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  (
( A  =  (/)  /\  B  =  (/) )  \/  ( -.  A  =  (/)  /\  -.  B  =  (/) ) ) )
51 dfbi3 863 . . . . . . . . 9  |-  ( ( A  =  (/)  <->  B  =  (/) )  <->  ( ( A  =  (/)  /\  B  =  (/) )  \/  ( -.  A  =  (/)  /\  -.  B  =  (/) ) ) )
5250, 51sylibr 203 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  =  (/)  <->  B  =  (/) ) )
53 nfre1 2612 . . . . . . . . . 10  |-  F/ y E. y  e.  B  ph
54 nfv 1609 . . . . . . . . . 10  |-  F/ y  x  =  z
5553, 54nfim 1781 . . . . . . . . 9  |-  F/ y ( E. y  e.  B  ph  ->  x  =  z )
56 nfre1 2612 . . . . . . . . . 10  |-  F/ x E. x  e.  A  ph
57 nfv 1609 . . . . . . . . . 10  |-  F/ x  y  =  w
5856, 57nfim 1781 . . . . . . . . 9  |-  F/ x
( E. x  e.  A  ph  ->  y  =  w )
5955, 58raaan2 28056 . . . . . . . 8  |-  ( ( A  =  (/)  <->  B  =  (/) )  ->  ( A. x  e.  A  A. y  e.  B  (
( E. y  e.  B  ph  ->  x  =  z )  /\  ( E. x  e.  A  ph 
->  y  =  w
) )  <->  ( A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
)  /\  A. y  e.  B  ( E. x  e.  A  ph  ->  y  =  w ) ) ) )
6052, 59syl 15 . . . . . . 7  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A. x  e.  A  A. y  e.  B  ( ( E. y  e.  B  ph  ->  x  =  z )  /\  ( E. x  e.  A  ph 
->  y  =  w
) )  <->  ( A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
)  /\  A. y  e.  B  ( E. x  e.  A  ph  ->  y  =  w ) ) ) )
6160adantr 451 . . . . . 6  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. x  e.  A  A. y  e.  B  (
( E. y  e.  B  ph  ->  x  =  z )  /\  ( E. x  e.  A  ph 
->  y  =  w
) )  <->  ( A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
)  /\  A. y  e.  B  ( E. x  e.  A  ph  ->  y  =  w ) ) ) )
6239, 44, 613bitrd 270 . . . . 5  |-  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  /\  (
z  e.  A  /\  w  e.  B )
)  ->  ( A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  ( A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
)  /\  A. y  e.  B  ( E. x  e.  A  ph  ->  y  =  w ) ) ) )
63622rexbidva 2597 . . . 4  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( E. z  e.  A  E. w  e.  B  A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  E. z  e.  A  E. w  e.  B  ( A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
)  /\  A. y  e.  B  ( E. x  e.  A  ph  ->  y  =  w ) ) ) )
64 reeanv 2720 . . . 4  |-  ( E. z  e.  A  E. w  e.  B  ( A. x  e.  A  ( E. y  e.  B  ph 
->  x  =  z
)  /\  A. y  e.  B  ( E. x  e.  A  ph  ->  y  =  w ) )  <-> 
( E. z  e.  A  A. x  e.  A  ( E. y  e.  B  ph  ->  x  =  z )  /\  E. w  e.  B  A. y  e.  B  ( E. x  e.  A  ph 
->  y  =  w
) ) )
6563, 64syl6rbb 253 . . 3  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  (
( E. z  e.  A  A. x  e.  A  ( E. y  e.  B  ph  ->  x  =  z )  /\  E. w  e.  B  A. y  e.  B  ( E. x  e.  A  ph 
->  y  =  w
) )  <->  E. z  e.  A  E. w  e.  B  A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
6611, 65anbi12d 691 . 2  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  (
( ( E. x  e.  A  E. y  e.  B  ph  /\  E. y  e.  B  E. x  e.  A  ph )  /\  ( E. z  e.  A  A. x  e.  A  ( E. y  e.  B  ph  ->  x  =  z )  /\  E. w  e.  B  A. y  e.  B  ( E. x  e.  A  ph 
->  y  =  w
) ) )  <->  ( E. x  e.  A  E. y  e.  B  ph  /\  E. z  e.  A  E. w  e.  B  A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) ) )
674, 6, 663bitrd 270 1  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  (
( 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. z  e.  A  E. w  e.  B  A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    = wceq 1632    e. wcel 1696    =/= wne 2459   A.wral 2556   E.wrex 2557   E!wreu 2558   (/)c0 3468
This theorem is referenced by:  2reu4  28071
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-v 2803  df-dif 3168  df-nul 3469
  Copyright terms: Public domain W3C validator