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 38001
Description: Definition of double restricted existential uniqueness ("exactly one  x and exactly one  y"), analogous to 2eu4 2358 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 38002). (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 3267 . . . 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 3267 . . . 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 701 . . 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 831 . . 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 2997 . . . . . 6  |-  ( E. y  e.  B  E. x  e.  A  ph  <->  E. x  e.  A  E. y  e.  B  ph )
87anbi2i 698 . . . . 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 648 . . . . 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 252 . . . 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 2962 . . . . . . . 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 2813 . . . . . . . . . . . . . 14  |-  F/ x A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w )
1413r19.3rz 3894 . . . . . . . . . . . . 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 204 . . . . . . . . . . . 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 466 . . . . . . . . . . 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 466 . . . . . . . . . 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 708 . . . . . . . . 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 871 . . . . . . . . . . . . . 14  |-  ( (
ph  ->  ( x  =  z  /\  y  =  w ) )  <->  ( ( ph  ->  x  =  z )  /\  ( ph  ->  y  =  w ) ) )
2019ralbii 2863 . . . . . . . . . . . . 13  |-  ( A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  A. y  e.  B  ( ( ph  ->  x  =  z )  /\  ( ph  ->  y  =  w ) ) )
21 r19.26 2962 . . . . . . . . . . . . 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 252 . . . . . . . . . . . 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 2863 . . . . . . . . . . 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 2962 . . . . . . . . . . 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 252 . . . . . . . . . 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 259 . . . . . . . 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 261 . . . . . . 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 2962 . . . . . . . . 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 2813 . . . . . . . . . . . . 13  |-  F/ y A. y  e.  B  ( ph  ->  x  =  z )
3130r19.3rz 3894 . . . . . . . . . . . 12  |-  ( B  =/=  (/)  ->  ( A. y  e.  B  ( ph  ->  x  =  z )  <->  A. y  e.  B  A. y  e.  B  ( ph  ->  x  =  z ) ) )
3231ad2antlr 731 . . . . . . . . . . 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 204 . . . . . . . . . 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 2996 . . . . . . . . . . 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 715 . . . . . . . . 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 260 . . . . . . . 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 2871 . . . . . . 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 259 . . . . . 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 2912 . . . . . . . . 9  |-  ( A. y  e.  B  ( ph  ->  x  =  z )  <->  ( E. y  e.  B  ph  ->  x  =  z ) )
41 r19.23v 2912 . . . . . . . . 9  |-  ( A. x  e.  A  ( ph  ->  y  =  w )  <->  ( E. x  e.  A  ph  ->  y  =  w ) )
4240, 41anbi12i 701 . . . . . . . 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 2864 . . . . . . 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 2627 . . . . . . . . . . . 12  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
4645biimpi 197 . . . . . . . . . . 11  |-  ( A  =/=  (/)  ->  -.  A  =  (/) )
47 df-ne 2627 . . . . . . . . . . . 12  |-  ( B  =/=  (/)  <->  -.  B  =  (/) )
4847biimpi 197 . . . . . . . . . . 11  |-  ( B  =/=  (/)  ->  -.  B  =  (/) )
4946, 48anim12i 568 . . . . . . . . . 10  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( -.  A  =  (/)  /\  -.  B  =  (/) ) )
5049olcd 394 . . . . . . . . 9  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  (
( A  =  (/)  /\  B  =  (/) )  \/  ( -.  A  =  (/)  /\  -.  B  =  (/) ) ) )
51 dfbi3 901 . . . . . . . . 9  |-  ( ( A  =  (/)  <->  B  =  (/) )  <->  ( ( A  =  (/)  /\  B  =  (/) )  \/  ( -.  A  =  (/)  /\  -.  B  =  (/) ) ) )
5250, 51sylibr 215 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  =  (/)  <->  B  =  (/) ) )
53 nfre1 2893 . . . . . . . . . 10  |-  F/ y E. y  e.  B  ph
54 nfv 1754 . . . . . . . . . 10  |-  F/ y  x  =  z
5553, 54nfim 1978 . . . . . . . . 9  |-  F/ y ( E. y  e.  B  ph  ->  x  =  z )
56 nfre1 2893 . . . . . . . . . 10  |-  F/ x E. x  e.  A  ph
57 nfv 1754 . . . . . . . . . 10  |-  F/ x  y  =  w
5856, 57nfim 1978 . . . . . . . . 9  |-  F/ x
( E. x  e.  A  ph  ->  y  =  w )
5955, 58raaan2 37987 . . . . . . . 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 17 . . . . . . 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 466 . . . . . 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 282 . . . . 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 2952 . . . 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 3003 . . . 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 265 . . 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 715 . 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 282 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 187    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1870    =/= wne 2625   A.wral 2782   E.wrex 2783   E!wreu 2784   (/)c0 3767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-v 3089  df-dif 3445  df-nul 3768
This theorem is referenced by:  2reu4  38002
  Copyright terms: Public domain W3C validator