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

Theorem 2reu4a 32355
Description: Definition of double restricted existential uniqueness ("exactly one  x and exactly one  y"), analogous to 2eu4 2380 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 32356). (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 3289 . . . 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 3289 . . . 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 697 . . 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 824 . . 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 3019 . . . . . 6  |-  ( E. y  e.  B  E. x  e.  A  ph  <->  E. x  e.  A  E. y  e.  B  ph )
87anbi2i 694 . . . . 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 644 . . . . 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 249 . . . 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 2984 . . . . . . . 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 2838 . . . . . . . . . . . . . 14  |-  F/ x A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w )
1413r19.3rz 3923 . . . . . . . . . . . . 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 201 . . . . . . . . . . . 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 465 . . . . . . . . . . 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 465 . . . . . . . . . 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 703 . . . . . . . . 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 863 . . . . . . . . . . . . . 14  |-  ( (
ph  ->  ( x  =  z  /\  y  =  w ) )  <->  ( ( ph  ->  x  =  z )  /\  ( ph  ->  y  =  w ) ) )
2019ralbii 2888 . . . . . . . . . . . . 13  |-  ( A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  A. y  e.  B  ( ( ph  ->  x  =  z )  /\  ( ph  ->  y  =  w ) ) )
21 r19.26 2984 . . . . . . . . . . . . 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 249 . . . . . . . . . . . 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 2888 . . . . . . . . . . 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 2984 . . . . . . . . . . 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 249 . . . . . . . . . 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 256 . . . . . . . 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 258 . . . . . . 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 2984 . . . . . . . . 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 2838 . . . . . . . . . . . . 13  |-  F/ y A. y  e.  B  ( ph  ->  x  =  z )
3130r19.3rz 3923 . . . . . . . . . . . 12  |-  ( B  =/=  (/)  ->  ( A. y  e.  B  ( ph  ->  x  =  z )  <->  A. y  e.  B  A. y  e.  B  ( ph  ->  x  =  z ) ) )
3231ad2antlr 726 . . . . . . . . . . 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 201 . . . . . . . . . 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 3018 . . . . . . . . . . 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 710 . . . . . . . . 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 257 . . . . . . . 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 2896 . . . . . . 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 256 . . . . . 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 2937 . . . . . . . . 9  |-  ( A. y  e.  B  ( ph  ->  x  =  z )  <->  ( E. y  e.  B  ph  ->  x  =  z ) )
41 r19.23v 2937 . . . . . . . . 9  |-  ( A. x  e.  A  ( ph  ->  y  =  w )  <->  ( E. x  e.  A  ph  ->  y  =  w ) )
4240, 41anbi12i 697 . . . . . . . 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 2889 . . . . . . 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 2654 . . . . . . . . . . . 12  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
4645biimpi 194 . . . . . . . . . . 11  |-  ( A  =/=  (/)  ->  -.  A  =  (/) )
47 df-ne 2654 . . . . . . . . . . . 12  |-  ( B  =/=  (/)  <->  -.  B  =  (/) )
4847biimpi 194 . . . . . . . . . . 11  |-  ( B  =/=  (/)  ->  -.  B  =  (/) )
4946, 48anim12i 566 . . . . . . . . . 10  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( -.  A  =  (/)  /\  -.  B  =  (/) ) )
5049olcd 393 . . . . . . . . 9  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  (
( A  =  (/)  /\  B  =  (/) )  \/  ( -.  A  =  (/)  /\  -.  B  =  (/) ) ) )
51 dfbi3 893 . . . . . . . . 9  |-  ( ( A  =  (/)  <->  B  =  (/) )  <->  ( ( A  =  (/)  /\  B  =  (/) )  \/  ( -.  A  =  (/)  /\  -.  B  =  (/) ) ) )
5250, 51sylibr 212 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  =  (/)  <->  B  =  (/) ) )
53 nfre1 2918 . . . . . . . . . 10  |-  F/ y E. y  e.  B  ph
54 nfv 1708 . . . . . . . . . 10  |-  F/ y  x  =  z
5553, 54nfim 1921 . . . . . . . . 9  |-  F/ y ( E. y  e.  B  ph  ->  x  =  z )
56 nfre1 2918 . . . . . . . . . 10  |-  F/ x E. x  e.  A  ph
57 nfv 1708 . . . . . . . . . 10  |-  F/ x  y  =  w
5856, 57nfim 1921 . . . . . . . . 9  |-  F/ x
( E. x  e.  A  ph  ->  y  =  w )
5955, 58raaan2 32341 . . . . . . . 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 465 . . . . . 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 279 . . . . 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 2974 . . . 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 3025 . . . 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 262 . . 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 710 . 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 279 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1395    e. wcel 1819    =/= wne 2652   A.wral 2807   E.wrex 2808   E!wreu 2809   (/)c0 3793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-v 3111  df-dif 3474  df-nul 3794
This theorem is referenced by:  2reu4  32356
  Copyright terms: Public domain W3C validator