MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2eu6 Unicode version

Theorem 2eu6 2228
Description: Two equivalent expressions for double existential uniqueness. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.)
Assertion
Ref Expression
2eu6  |-  ( ( E! x E. y ph  /\  E! y E. x ph )  <->  E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w ) ) )
Distinct variable groups:    x, y,
z, w    ph, z, w
Allowed substitution hints:    ph( x, y)

Proof of Theorem 2eu6
Dummy variables  v  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2eu4 2226 . 2  |-  ( ( E! x E. y ph  /\  E! y E. x ph )  <->  ( E. x E. y ph  /\  E. z E. w A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
2 nfv 1605 . . . . . 6  |-  F/ z
ph
3 nfv 1605 . . . . . 6  |-  F/ w ph
4 nfs1v 2045 . . . . . 6  |-  F/ x [ z  /  x ] [ w  /  y ] ph
5 nfs1v 2045 . . . . . . 7  |-  F/ y [ w  /  y ] ph
65nfsb 2048 . . . . . 6  |-  F/ y [ z  /  x ] [ w  /  y ] ph
7 sbequ12 1860 . . . . . . 7  |-  ( y  =  w  ->  ( ph 
<->  [ w  /  y ] ph ) )
8 sbequ12 1860 . . . . . . 7  |-  ( x  =  z  ->  ( [ w  /  y ] ph  <->  [ z  /  x ] [ w  /  y ] ph ) )
97, 8sylan9bbr 681 . . . . . 6  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ph  <->  [ z  /  x ] [ w  /  y ] ph ) )
102, 3, 4, 6, 9cbvex2 1945 . . . . 5  |-  ( E. x E. y ph  <->  E. z E. w [
z  /  x ] [ w  /  y ] ph )
11 equequ2 1649 . . . . . . . . . 10  |-  ( z  =  v  ->  (
x  =  z  <->  x  =  v ) )
12 equequ2 1649 . . . . . . . . . 10  |-  ( w  =  u  ->  (
y  =  w  <->  y  =  u ) )
1311, 12bi2anan9 843 . . . . . . . . 9  |-  ( ( z  =  v  /\  w  =  u )  ->  ( ( x  =  z  /\  y  =  w )  <->  ( x  =  v  /\  y  =  u ) ) )
1413imbi2d 307 . . . . . . . 8  |-  ( ( z  =  v  /\  w  =  u )  ->  ( ( ph  ->  ( x  =  z  /\  y  =  w )
)  <->  ( ph  ->  ( x  =  v  /\  y  =  u )
) ) )
15142albidv 1613 . . . . . . 7  |-  ( ( z  =  v  /\  w  =  u )  ->  ( A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
)  <->  A. x A. y
( ph  ->  ( x  =  v  /\  y  =  u ) ) ) )
1615cbvex2v 1947 . . . . . 6  |-  ( E. z E. w A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  E. v E. u A. x A. y ( ph  ->  ( x  =  v  /\  y  =  u )
) )
17 nfv 1605 . . . . . . . . 9  |-  F/ z ( ph  ->  (
x  =  v  /\  y  =  u )
)
18 nfv 1605 . . . . . . . . 9  |-  F/ w
( ph  ->  ( x  =  v  /\  y  =  u ) )
19 nfv 1605 . . . . . . . . . 10  |-  F/ x
( z  =  v  /\  w  =  u )
204, 19nfim 1769 . . . . . . . . 9  |-  F/ x
( [ z  /  x ] [ w  / 
y ] ph  ->  ( z  =  v  /\  w  =  u )
)
21 nfv 1605 . . . . . . . . . 10  |-  F/ y ( z  =  v  /\  w  =  u )
226, 21nfim 1769 . . . . . . . . 9  |-  F/ y ( [ z  /  x ] [ w  / 
y ] ph  ->  ( z  =  v  /\  w  =  u )
)
23 equequ1 1648 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
x  =  v  <->  z  =  v ) )
24 equequ1 1648 . . . . . . . . . . 11  |-  ( y  =  w  ->  (
y  =  u  <->  w  =  u ) )
2523, 24bi2anan9 843 . . . . . . . . . 10  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ( x  =  v  /\  y  =  u )  <->  ( z  =  v  /\  w  =  u ) ) )
269, 25imbi12d 311 . . . . . . . . 9  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ( ph  ->  ( x  =  v  /\  y  =  u )
)  <->  ( [ z  /  x ] [
w  /  y ]
ph  ->  ( z  =  v  /\  w  =  u ) ) ) )
2717, 18, 20, 22, 26cbval2 1944 . . . . . . . 8  |-  ( A. x A. y ( ph  ->  ( x  =  v  /\  y  =  u ) )  <->  A. z A. w ( [ z  /  x ] [
w  /  y ]
ph  ->  ( z  =  v  /\  w  =  u ) ) )
28272exbii 1570 . . . . . . 7  |-  ( E. v E. u A. x A. y ( ph  ->  ( x  =  v  /\  y  =  u ) )  <->  E. v E. u A. z A. w ( [ z  /  x ] [
w  /  y ]
ph  ->  ( z  =  v  /\  w  =  u ) ) )
29 2mo 2221 . . . . . . 7  |-  ( E. v E. u A. z A. w ( [ z  /  x ] [ w  /  y ] ph  ->  ( z  =  v  /\  w  =  u ) )  <->  A. z A. w A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) )
3028, 29bitri 240 . . . . . 6  |-  ( E. v E. u A. x A. y ( ph  ->  ( x  =  v  /\  y  =  u ) )  <->  A. z A. w A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) )
3116, 30bitri 240 . . . . 5  |-  ( E. z E. w A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w ) )  <->  A. z A. w A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) )
32 19.29r2 1585 . . . . 5  |-  ( ( E. z E. w [ z  /  x ] [ w  /  y ] ph  /\  A. z A. w A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) )  ->  E. z E. w ( [ z  /  x ] [
w  /  y ]
ph  /\  A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) ) )
3310, 31, 32syl2anb 465 . . . 4  |-  ( ( E. x E. y ph  /\  E. z E. w A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) )  ->  E. z E. w ( [ z  /  x ] [
w  /  y ]
ph  /\  A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) ) )
34 2albiim 1599 . . . . . . 7  |-  ( A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  <->  ( A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
)  /\  A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph )
) )
35 ancom 437 . . . . . . 7  |-  ( ( A. x A. y
( ph  ->  ( x  =  z  /\  y  =  w ) )  /\  A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph ) )  <-> 
( A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph )  /\  A. x A. y
( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
3634, 35bitri 240 . . . . . 6  |-  ( A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  <->  ( A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph )  /\  A. x A. y
( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
37362exbii 1570 . . . . 5  |-  ( E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  <->  E. z E. w
( A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph )  /\  A. x A. y
( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
38 nfv 1605 . . . . . . . . . . . 12  |-  F/ v ( ( [ z  /  x ] [
w  /  y ]
ph  /\  ph )  -> 
( z  =  x  /\  w  =  y ) )
39 nfv 1605 . . . . . . . . . . . 12  |-  F/ u
( ( [ z  /  x ] [
w  /  y ]
ph  /\  ph )  -> 
( z  =  x  /\  w  =  y ) )
404nfsb 2048 . . . . . . . . . . . . . . 15  |-  F/ x [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
4140nfsb 2048 . . . . . . . . . . . . . 14  |-  F/ x [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
424, 41nfan 1771 . . . . . . . . . . . . 13  |-  F/ x
( [ z  /  x ] [ w  / 
y ] ph  /\  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
4342, 19nfim 1769 . . . . . . . . . . . 12  |-  F/ x
( ( [ z  /  x ] [
w  /  y ]
ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
)
446nfsb 2048 . . . . . . . . . . . . . . 15  |-  F/ y [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
4544nfsb 2048 . . . . . . . . . . . . . 14  |-  F/ y [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
466, 45nfan 1771 . . . . . . . . . . . . 13  |-  F/ y ( [ z  /  x ] [ w  / 
y ] ph  /\  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
4746, 21nfim 1769 . . . . . . . . . . . 12  |-  F/ y ( ( [ z  /  x ] [
w  /  y ]
ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
)
48 sbequ12 1860 . . . . . . . . . . . . . . . 16  |-  ( y  =  u  ->  ( ph 
<->  [ u  /  y ] ph ) )
49 sbequ12 1860 . . . . . . . . . . . . . . . 16  |-  ( x  =  v  ->  ( [ u  /  y ] ph  <->  [ v  /  x ] [ u  /  y ] ph ) )
5048, 49sylan9bbr 681 . . . . . . . . . . . . . . 15  |-  ( ( x  =  v  /\  y  =  u )  ->  ( ph  <->  [ v  /  x ] [ u  /  y ] ph ) )
513sbco2 2026 . . . . . . . . . . . . . . . . 17  |-  ( [ u  /  w ] [ w  /  y ] ph  <->  [ u  /  y ] ph )
5251sbbii 1634 . . . . . . . . . . . . . . . 16  |-  ( [ v  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  x ] [ u  /  y ] ph )
53 nfv 1605 . . . . . . . . . . . . . . . . . 18  |-  F/ z [ u  /  w ] [ w  /  y ] ph
5453sbco2 2026 . . . . . . . . . . . . . . . . 17  |-  ( [ v  /  z ] [ z  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  x ] [ u  /  w ] [ w  /  y ] ph )
55 sbcom2 2053 . . . . . . . . . . . . . . . . . 18  |-  ( [ z  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5655sbbii 1634 . . . . . . . . . . . . . . . . 17  |-  ( [ v  /  z ] [ z  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5754, 56bitr3i 242 . . . . . . . . . . . . . . . 16  |-  ( [ v  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5852, 57bitr3i 242 . . . . . . . . . . . . . . 15  |-  ( [ v  /  x ] [ u  /  y ] ph  <->  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5950, 58syl6bb 252 . . . . . . . . . . . . . 14  |-  ( ( x  =  v  /\  y  =  u )  ->  ( ph  <->  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph ) )
6059anbi2d 684 . . . . . . . . . . . . 13  |-  ( ( x  =  v  /\  y  =  u )  ->  ( ( [ z  /  x ] [
w  /  y ]
ph  /\  ph )  <->  ( [
z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph ) ) )
61 equequ2 1649 . . . . . . . . . . . . . 14  |-  ( x  =  v  ->  (
z  =  x  <->  z  =  v ) )
62 equequ2 1649 . . . . . . . . . . . . . 14  |-  ( y  =  u  ->  (
w  =  y  <->  w  =  u ) )
6361, 62bi2anan9 843 . . . . . . . . . . . . 13  |-  ( ( x  =  v  /\  y  =  u )  ->  ( ( z  =  x  /\  w  =  y )  <->  ( z  =  v  /\  w  =  u ) ) )
6460, 63imbi12d 311 . . . . . . . . . . . 12  |-  ( ( x  =  v  /\  y  =  u )  ->  ( ( ( [ z  /  x ] [ w  /  y ] ph  /\  ph )  ->  ( z  =  x  /\  w  =  y ) )  <->  ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) ) )
6538, 39, 43, 47, 64cbval2 1944 . . . . . . . . . . 11  |-  ( A. x A. y ( ( [ z  /  x ] [ w  /  y ] ph  /\  ph )  ->  ( z  =  x  /\  w  =  y ) )  <->  A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) )
66 equcom 1647 . . . . . . . . . . . . . . 15  |-  ( z  =  x  <->  x  =  z )
67 equcom 1647 . . . . . . . . . . . . . . 15  |-  ( w  =  y  <->  y  =  w )
6866, 67anbi12i 678 . . . . . . . . . . . . . 14  |-  ( ( z  =  x  /\  w  =  y )  <->  ( x  =  z  /\  y  =  w )
)
6968imbi2i 303 . . . . . . . . . . . . 13  |-  ( ( ( [ z  /  x ] [ w  / 
y ] ph  /\  ph )  ->  ( z  =  x  /\  w  =  y ) )  <-> 
( ( [ z  /  x ] [
w  /  y ]
ph  /\  ph )  -> 
( x  =  z  /\  y  =  w ) ) )
70 impexp 433 . . . . . . . . . . . . 13  |-  ( ( ( [ z  /  x ] [ w  / 
y ] ph  /\  ph )  ->  ( x  =  z  /\  y  =  w ) )  <->  ( [
z  /  x ] [ w  /  y ] ph  ->  ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
7169, 70bitri 240 . . . . . . . . . . . 12  |-  ( ( ( [ z  /  x ] [ w  / 
y ] ph  /\  ph )  ->  ( z  =  x  /\  w  =  y ) )  <-> 
( [ z  /  x ] [ w  / 
y ] ph  ->  (
ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
72712albii 1554 . . . . . . . . . . 11  |-  ( A. x A. y ( ( [ z  /  x ] [ w  /  y ] ph  /\  ph )  ->  ( z  =  x  /\  w  =  y ) )  <->  A. x A. y ( [ z  /  x ] [
w  /  y ]
ph  ->  ( ph  ->  ( x  =  z  /\  y  =  w )
) ) )
7365, 72bitr3i 242 . . . . . . . . . 10  |-  ( A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
)  <->  A. x A. y
( [ z  /  x ] [ w  / 
y ] ph  ->  (
ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
744, 619.21-2 1792 . . . . . . . . . 10  |-  ( A. x A. y ( [ z  /  x ] [ w  /  y ] ph  ->  ( ph  ->  ( x  =  z  /\  y  =  w ) ) )  <->  ( [
z  /  x ] [ w  /  y ] ph  ->  A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) ) )
7573, 74bitri 240 . . . . . . . . 9  |-  ( A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
)  <->  ( [ z  /  x ] [
w  /  y ]
ph  ->  A. x A. y
( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
7675anbi2i 675 . . . . . . . 8  |-  ( ( [ z  /  x ] [ w  /  y ] ph  /\  A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) )  <->  ( [
z  /  x ] [ w  /  y ] ph  /\  ( [ z  /  x ] [ w  /  y ] ph  ->  A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) ) ) )
77 abai 770 . . . . . . . 8  |-  ( ( [ z  /  x ] [ w  /  y ] ph  /\  A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) )  <->  ( [
z  /  x ] [ w  /  y ] ph  /\  ( [ z  /  x ] [ w  /  y ] ph  ->  A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) ) ) )
7876, 77bitr4i 243 . . . . . . 7  |-  ( ( [ z  /  x ] [ w  /  y ] ph  /\  A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) )  <->  ( [
z  /  x ] [ w  /  y ] ph  /\  A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) ) )
79 2sb6 2052 . . . . . . . 8  |-  ( [ z  /  x ] [ w  /  y ] ph  <->  A. x A. y
( ( x  =  z  /\  y  =  w )  ->  ph )
)
8079anbi1i 676 . . . . . . 7  |-  ( ( [ z  /  x ] [ w  /  y ] ph  /\  A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) )  <->  ( A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph )  /\  A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
8178, 80bitri 240 . . . . . 6  |-  ( ( [ z  /  x ] [ w  /  y ] ph  /\  A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) )  <->  ( A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph )  /\  A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
82812exbii 1570 . . . . 5  |-  ( E. z E. w ( [ z  /  x ] [ w  /  y ] ph  /\  A. v A. u ( ( [ z  /  x ] [ w  /  y ] ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) )  <->  E. z E. w ( A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph )  /\  A. x A. y
( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
8337, 82bitr4i 243 . . . 4  |-  ( E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  <->  E. z E. w
( [ z  /  x ] [ w  / 
y ] ph  /\  A. v A. u ( ( [ z  /  x ] [ w  / 
y ] ph  /\  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
) ) )
8433, 83sylibr 203 . . 3  |-  ( ( E. x E. y ph  /\  E. z E. w A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) )  ->  E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w ) ) )
85 bi2 189 . . . . . . 7  |-  ( (
ph 
<->  ( x  =  z  /\  y  =  w ) )  ->  (
( x  =  z  /\  y  =  w )  ->  ph ) )
86852alimi 1547 . . . . . 6  |-  ( A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  ->  A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph )
)
87862eximi 1564 . . . . 5  |-  ( E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  ->  E. z E. w A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph )
)
88 2exsb 2071 . . . . 5  |-  ( E. x E. y ph  <->  E. z E. w A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph ) )
8987, 88sylibr 203 . . . 4  |-  ( E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  ->  E. x E. y ph )
90 bi1 178 . . . . . 6  |-  ( (
ph 
<->  ( x  =  z  /\  y  =  w ) )  ->  ( ph  ->  ( x  =  z  /\  y  =  w ) ) )
91902alimi 1547 . . . . 5  |-  ( A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  ->  A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) )
92912eximi 1564 . . . 4  |-  ( E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  ->  E. z E. w A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) )
9389, 92jca 518 . . 3  |-  ( E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  ->  ( E. x E. y ph  /\  E. z E. w A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
9484, 93impbii 180 . 2  |-  ( ( E. x E. y ph  /\  E. z E. w A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) )  <->  E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w ) ) )
951, 94bitri 240 1  |-  ( ( E! x E. y ph  /\  E! y E. x ph )  <->  E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527   E.wex 1528    = wceq 1623   [wsb 1629   E!weu 2143
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
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
  Copyright terms: Public domain W3C validator