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

Theorem 2reu4a 27834
Description: Definition of double restricted existential uniqueness ("exactly one  x and exactly one  y"), analogous to 2eu4 2337 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 27835). (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 3084 . . . 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 3084 . . . 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 679 . . 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 11 . 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 798 . . 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 11 . 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 2829 . . . . . 6  |-  ( E. y  e.  B  E. x  e.  A  ph  <->  E. x  e.  A  E. y  e.  B  ph )
87anbi2i 676 . . . . 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 626 . . . . 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 241 . . . 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 11 . . 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 2798 . . . . . . . 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 2716 . . . . . . . . . . . . . 14  |-  F/ x A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w )
1413r19.3rz 3679 . . . . . . . . . . . . 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 193 . . . . . . . . . . . 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 452 . . . . . . . . . . 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 452 . . . . . . . . . 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 685 . . . . . . . . 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 834 . . . . . . . . . . . . . 14  |-  ( (
ph  ->  ( x  =  z  /\  y  =  w ) )  <->  ( ( ph  ->  x  =  z )  /\  ( ph  ->  y  =  w ) ) )
2019ralbii 2690 . . . . . . . . . . . . 13  |-  ( A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  A. y  e.  B  ( ( ph  ->  x  =  z )  /\  ( ph  ->  y  =  w ) ) )
21 r19.26 2798 . . . . . . . . . . . . 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 241 . . . . . . . . . . . 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 2690 . . . . . . . . . . 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 2798 . . . . . . . . . . 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 241 . . . . . . . . . 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 11 . . . . . . . . 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 248 . . . . . . . 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 250 . . . . . . 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 2798 . . . . . . . . 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 2716 . . . . . . . . . . . . 13  |-  F/ y A. y  e.  B  ( ph  ->  x  =  z )
3130r19.3rz 3679 . . . . . . . . . . . 12  |-  ( B  =/=  (/)  ->  ( A. y  e.  B  ( ph  ->  x  =  z )  <->  A. y  e.  B  A. y  e.  B  ( ph  ->  x  =  z ) ) )
3231ad2antlr 708 . . . . . . . . . . 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 193 . . . . . . . . . 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 2828 . . . . . . . . . . 11  |-  ( A. y  e.  B  A. x  e.  A  ( ph  ->  y  =  w )  <->  A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w ) )
3534a1i 11 . . . . . . . . . 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 692 . . . . . . . . 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 249 . . . . . . . 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 2686 . . . . . . 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 248 . . . . . 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 2782 . . . . . . . . 9  |-  ( A. y  e.  B  ( ph  ->  x  =  z )  <->  ( E. y  e.  B  ph  ->  x  =  z ) )
41 r19.23v 2782 . . . . . . . . 9  |-  ( A. x  e.  A  ( ph  ->  y  =  w )  <->  ( E. x  e.  A  ph  ->  y  =  w ) )
4240, 41anbi12i 679 . . . . . . . 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 2692 . . . . . . 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 11 . . . . . 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 2569 . . . . . . . . . . . 12  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
4645biimpi 187 . . . . . . . . . . 11  |-  ( A  =/=  (/)  ->  -.  A  =  (/) )
47 df-ne 2569 . . . . . . . . . . . 12  |-  ( B  =/=  (/)  <->  -.  B  =  (/) )
4847biimpi 187 . . . . . . . . . . 11  |-  ( B  =/=  (/)  ->  -.  B  =  (/) )
4946, 48anim12i 550 . . . . . . . . . 10  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( -.  A  =  (/)  /\  -.  B  =  (/) ) )
5049olcd 383 . . . . . . . . 9  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  (
( A  =  (/)  /\  B  =  (/) )  \/  ( -.  A  =  (/)  /\  -.  B  =  (/) ) ) )
51 dfbi3 864 . . . . . . . . 9  |-  ( ( A  =  (/)  <->  B  =  (/) )  <->  ( ( A  =  (/)  /\  B  =  (/) )  \/  ( -.  A  =  (/)  /\  -.  B  =  (/) ) ) )
5250, 51sylibr 204 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  =  (/)  <->  B  =  (/) ) )
53 nfre1 2722 . . . . . . . . . 10  |-  F/ y E. y  e.  B  ph
54 nfv 1626 . . . . . . . . . 10  |-  F/ y  x  =  z
5553, 54nfim 1828 . . . . . . . . 9  |-  F/ y ( E. y  e.  B  ph  ->  x  =  z )
56 nfre1 2722 . . . . . . . . . 10  |-  F/ x E. x  e.  A  ph
57 nfv 1626 . . . . . . . . . 10  |-  F/ x  y  =  w
5856, 57nfim 1828 . . . . . . . . 9  |-  F/ x
( E. x  e.  A  ph  ->  y  =  w )
5955, 58raaan2 27820 . . . . . . . 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 16 . . . . . . 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 452 . . . . . 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 271 . . . . 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 2707 . . . 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 2835 . . . 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 254 . . 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 692 . 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 271 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 177    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1721    =/= wne 2567   A.wral 2666   E.wrex 2667   E!wreu 2668   (/)c0 3588
This theorem is referenced by:  2reu4  27835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-v 2918  df-dif 3283  df-nul 3589
  Copyright terms: Public domain W3C validator