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

Theorem 2eu6 2201
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
StepHypRef Expression
1 2eu4 2199 . 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 1629 . . . . . 6  |-  F/ z
ph
3 nfv 1629 . . . . . 6  |-  F/ w ph
4 nfs1v 2069 . . . . . 6  |-  F/ x [ z  /  x ] [ w  /  y ] ph
5 nfs1v 2069 . . . . . . 7  |-  F/ y [ w  /  y ] ph
65nfsb 2072 . . . . . 6  |-  F/ y [ z  /  x ] [ w  /  y ] ph
7 sbequ12 1893 . . . . . . 7  |-  ( y  =  w  ->  ( ph 
<->  [ w  /  y ] ph ) )
8 sbequ12 1893 . . . . . . 7  |-  ( x  =  z  ->  ( [ w  /  y ] ph  <->  [ z  /  x ] [ w  /  y ] ph ) )
97, 8sylan9bbr 684 . . . . . 6  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ph  <->  [ z  /  x ] [ w  /  y ] ph ) )
102, 3, 4, 6, 9cbvex2 2049 . . . . 5  |-  ( E. x E. y ph  <->  E. z E. w [
z  /  x ] [ w  /  y ] ph )
11 equequ2 1830 . . . . . . . . . 10  |-  ( z  =  v  ->  (
x  =  z  <->  x  =  v ) )
12 equequ2 1830 . . . . . . . . . 10  |-  ( w  =  u  ->  (
y  =  w  <->  y  =  u ) )
1311, 12bi2anan9 848 . . . . . . . . 9  |-  ( ( z  =  v  /\  w  =  u )  ->  ( ( x  =  z  /\  y  =  w )  <->  ( x  =  v  /\  y  =  u ) ) )
1413imbi2d 309 . . . . . . . 8  |-  ( ( z  =  v  /\  w  =  u )  ->  ( ( ph  ->  ( x  =  z  /\  y  =  w )
)  <->  ( ph  ->  ( x  =  v  /\  y  =  u )
) ) )
15142albidv 2007 . . . . . . 7  |-  ( ( z  =  v  /\  w  =  u )  ->  ( A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
)  <->  A. x A. y
( ph  ->  ( x  =  v  /\  y  =  u ) ) ) )
1615cbvex2v 2051 . . . . . 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 1629 . . . . . . . . 9  |-  F/ z ( ph  ->  (
x  =  v  /\  y  =  u )
)
18 nfv 1629 . . . . . . . . 9  |-  F/ w
( ph  ->  ( x  =  v  /\  y  =  u ) )
19 nfv 1629 . . . . . . . . . 10  |-  F/ x
( z  =  v  /\  w  =  u )
204, 19nfim 1735 . . . . . . . . 9  |-  F/ x
( [ z  /  x ] [ w  / 
y ] ph  ->  ( z  =  v  /\  w  =  u )
)
21 nfv 1629 . . . . . . . . . 10  |-  F/ y ( z  =  v  /\  w  =  u )
226, 21nfim 1735 . . . . . . . . 9  |-  F/ y ( [ z  /  x ] [ w  / 
y ] ph  ->  ( z  =  v  /\  w  =  u )
)
23 equequ1 1829 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
x  =  v  <->  z  =  v ) )
24 equequ1 1829 . . . . . . . . . . 11  |-  ( y  =  w  ->  (
y  =  u  <->  w  =  u ) )
2523, 24bi2anan9 848 . . . . . . . . . 10  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ( x  =  v  /\  y  =  u )  <->  ( z  =  v  /\  w  =  u ) ) )
269, 25imbi12d 313 . . . . . . . . 9  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ( ph  ->  ( x  =  v  /\  y  =  u )
)  <->  ( [ z  /  x ] [
w  /  y ]
ph  ->  ( z  =  v  /\  w  =  u ) ) ) )
2717, 18, 20, 22, 26cbval2 2048 . . . . . . . 8  |-  ( A. x A. y ( ph  ->  ( x  =  v  /\  y  =  u ) )  <->  A. z A. w ( [ z  /  x ] [
w  /  y ]
ph  ->  ( z  =  v  /\  w  =  u ) ) )
28272exbii 1581 . . . . . . 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 2194 . . . . . . 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 242 . . . . . 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 242 . . . . 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 1597 . . . . 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 467 . . . 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 1613 . . . . . . 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 439 . . . . . . 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 242 . . . . . 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 1581 . . . . 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 1629 . . . . . . . . . . . 12  |-  F/ v ( ( [ z  /  x ] [
w  /  y ]
ph  /\  ph )  -> 
( z  =  x  /\  w  =  y ) )
39 nfv 1629 . . . . . . . . . . . 12  |-  F/ u
( ( [ z  /  x ] [
w  /  y ]
ph  /\  ph )  -> 
( z  =  x  /\  w  =  y ) )
404nfsb 2072 . . . . . . . . . . . . . . 15  |-  F/ x [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
4140nfsb 2072 . . . . . . . . . . . . . 14  |-  F/ x [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
424, 41nfan 1737 . . . . . . . . . . . . 13  |-  F/ x
( [ z  /  x ] [ w  / 
y ] ph  /\  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
4342, 19nfim 1735 . . . . . . . . . . . 12  |-  F/ x
( ( [ z  /  x ] [
w  /  y ]
ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
)
446nfsb 2072 . . . . . . . . . . . . . . 15  |-  F/ y [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
4544nfsb 2072 . . . . . . . . . . . . . 14  |-  F/ y [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
466, 45nfan 1737 . . . . . . . . . . . . 13  |-  F/ y ( [ z  /  x ] [ w  / 
y ] ph  /\  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
4746, 21nfim 1735 . . . . . . . . . . . 12  |-  F/ y ( ( [ z  /  x ] [
w  /  y ]
ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
)
48 sbequ12 1893 . . . . . . . . . . . . . . . 16  |-  ( y  =  u  ->  ( ph 
<->  [ u  /  y ] ph ) )
49 sbequ12 1893 . . . . . . . . . . . . . . . 16  |-  ( x  =  v  ->  ( [ u  /  y ] ph  <->  [ v  /  x ] [ u  /  y ] ph ) )
5048, 49sylan9bbr 684 . . . . . . . . . . . . . . 15  |-  ( ( x  =  v  /\  y  =  u )  ->  ( ph  <->  [ v  /  x ] [ u  /  y ] ph ) )
513sbco2 1981 . . . . . . . . . . . . . . . . 17  |-  ( [ u  /  w ] [ w  /  y ] ph  <->  [ u  /  y ] ph )
5251sbbii 1886 . . . . . . . . . . . . . . . 16  |-  ( [ v  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  x ] [ u  /  y ] ph )
53 nfv 1629 . . . . . . . . . . . . . . . . . 18  |-  F/ z [ u  /  w ] [ w  /  y ] ph
5453sbco2 1981 . . . . . . . . . . . . . . . . 17  |-  ( [ v  /  z ] [ z  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  x ] [ u  /  w ] [ w  /  y ] ph )
55 sbcom2 2077 . . . . . . . . . . . . . . . . . 18  |-  ( [ z  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5655sbbii 1886 . . . . . . . . . . . . . . . . 17  |-  ( [ v  /  z ] [ z  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5754, 56bitr3i 244 . . . . . . . . . . . . . . . 16  |-  ( [ v  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5852, 57bitr3i 244 . . . . . . . . . . . . . . 15  |-  ( [ v  /  x ] [ u  /  y ] ph  <->  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5950, 58syl6bb 254 . . . . . . . . . . . . . 14  |-  ( ( x  =  v  /\  y  =  u )  ->  ( ph  <->  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph ) )
6059anbi2d 687 . . . . . . . . . . . . 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 1830 . . . . . . . . . . . . . 14  |-  ( x  =  v  ->  (
z  =  x  <->  z  =  v ) )
62 equequ2 1830 . . . . . . . . . . . . . 14  |-  ( y  =  u  ->  (
w  =  y  <->  w  =  u ) )
6361, 62bi2anan9 848 . . . . . . . . . . . . 13  |-  ( ( x  =  v  /\  y  =  u )  ->  ( ( z  =  x  /\  w  =  y )  <->  ( z  =  v  /\  w  =  u ) ) )
6460, 63imbi12d 313 . . . . . . . . . . . 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 2048 . . . . . . . . . . 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 1824 . . . . . . . . . . . . . . 15  |-  ( z  =  x  <->  x  =  z )
67 equcom 1824 . . . . . . . . . . . . . . 15  |-  ( w  =  y  <->  y  =  w )
6866, 67anbi12i 681 . . . . . . . . . . . . . 14  |-  ( ( z  =  x  /\  w  =  y )  <->  ( x  =  z  /\  y  =  w )
)
6968imbi2i 305 . . . . . . . . . . . . 13  |-  ( ( ( [ z  /  x ] [ w  / 
y ] ph  /\  ph )  ->  ( z  =  x  /\  w  =  y ) )  <-> 
( ( [ z  /  x ] [
w  /  y ]
ph  /\  ph )  -> 
( x  =  z  /\  y  =  w ) ) )
70 impexp 435 . . . . . . . . . . . . 13  |-  ( ( ( [ z  /  x ] [ w  / 
y ] ph  /\  ph )  ->  ( x  =  z  /\  y  =  w ) )  <->  ( [
z  /  x ] [ w  /  y ] ph  ->  ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
7169, 70bitri 242 . . . . . . . . . . . 12  |-  ( ( ( [ z  /  x ] [ w  / 
y ] ph  /\  ph )  ->  ( z  =  x  /\  w  =  y ) )  <-> 
( [ z  /  x ] [ w  / 
y ] ph  ->  (
ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
72712albii 1555 . . . . . . . . . . 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 244 . . . . . . . . . 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 1772 . . . . . . . . . 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 242 . . . . . . . . 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 678 . . . . . . . 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 773 . . . . . . . 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 245 . . . . . . 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 2076 . . . . . . . 8  |-  ( [ z  /  x ] [ w  /  y ] ph  <->  A. x A. y
( ( x  =  z  /\  y  =  w )  ->  ph )
)
8079anbi1i 679 . . . . . . 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 242 . . . . . 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 1581 . . . . 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 245 . . . 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 205 . . 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 191 . . . . . . 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 1575 . . . . 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 2094 . . . . 5  |-  ( E. x E. y ph  <->  E. z E. w A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph ) )
8987, 88sylibr 205 . . . 4  |-  ( E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  ->  E. x E. y ph )
90 bi1 180 . . . . . 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 1575 . . . 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 520 . . 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 182 . 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 242 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 6    <-> wb 178    /\ wa 360   A.wal 1532   E.wex 1537    = wceq 1619   [wsb 1883   E!weu 2117
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121
  Copyright terms: Public domain W3C validator