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

Theorem 2reu4a 27967
Description: Definition of double restricted existential uniqueness ("exactly one  x and exactly one  y"), analogous to 2eu4 2226 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 27968). (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 2955 . . . 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 2955 . . . 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 2701 . . . . . 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 2675 . . . . . . . 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 2593 . . . . . . . . . . . . . 14  |-  F/ x A. x  e.  A  A. y  e.  B  ( ph  ->  y  =  w )
1413r19.3rz 3545 . . . . . . . . . . . . 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 2567 . . . . . . . . . . . . 13  |-  ( A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  A. y  e.  B  ( ( ph  ->  x  =  z )  /\  ( ph  ->  y  =  w ) ) )
21 r19.26 2675 . . . . . . . . . . . . 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 2567 . . . . . . . . . . 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 2675 . . . . . . . . . . 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 2675 . . . . . . . . 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 2593 . . . . . . . . . . . . 13  |-  F/ y A. y  e.  B  ( ph  ->  x  =  z )
3130r19.3rz 3545 . . . . . . . . . . . 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 2700 . . . . . . . . . . 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 2563 . . . . . . 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 2659 . . . . . . . . 9  |-  ( A. y  e.  B  ( ph  ->  x  =  z )  <->  ( E. y  e.  B  ph  ->  x  =  z ) )
41 r19.23v 2659 . . . . . . . . 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 2569 . . . . . . 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 2448 . . . . . . . . . . . 12  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
4645biimpi 186 . . . . . . . . . . 11  |-  ( A  =/=  (/)  ->  -.  A  =  (/) )
47 df-ne 2448 . . . . . . . . . . . 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 2599 . . . . . . . . . 10  |-  F/ y E. y  e.  B  ph
54 nfv 1605 . . . . . . . . . 10  |-  F/ y  x  =  z
5553, 54nfim 1769 . . . . . . . . 9  |-  F/ y ( E. y  e.  B  ph  ->  x  =  z )
56 nfre1 2599 . . . . . . . . . 10  |-  F/ x E. x  e.  A  ph
57 nfv 1605 . . . . . . . . . 10  |-  F/ x  y  =  w
5856, 57nfim 1769 . . . . . . . . 9  |-  F/ x
( E. x  e.  A  ph  ->  y  =  w )
5955, 58raaan2 27953 . . . . . . . 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 2584 . . . 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 2707 . . . 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 1623    e. wcel 1684    =/= wne 2446   A.wral 2543   E.wrex 2544   E!wreu 2545   (/)c0 3455
This theorem is referenced by:  2reu4  27968
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-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator