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

Theorem 2eu6OLD 2372
Description: Obsolete proof of 2eu6 2371 as of 21-Sep-2019. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
2eu6OLD  |-  ( ( 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 2eu6OLD
Dummy variables  v  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2eu4 2368 . 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 1673 . . . . . 6  |-  F/ z
ph
3 nfv 1673 . . . . . 6  |-  F/ w ph
4 nfs1v 2142 . . . . . 6  |-  F/ x [ z  /  x ] [ w  /  y ] ph
5 nfs1v 2142 . . . . . . 7  |-  F/ y [ w  /  y ] ph
65nfsb 2146 . . . . . 6  |-  F/ y [ z  /  x ] [ w  /  y ] ph
7 sbequ12 1936 . . . . . . 7  |-  ( y  =  w  ->  ( ph 
<->  [ w  /  y ] ph ) )
8 sbequ12 1936 . . . . . . 7  |-  ( x  =  z  ->  ( [ w  /  y ] ph  <->  [ z  /  x ] [ w  /  y ] ph ) )
97, 8sylan9bbr 700 . . . . . 6  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ph  <->  [ z  /  x ] [ w  /  y ] ph ) )
102, 3, 4, 6, 9cbvex2 1976 . . . . 5  |-  ( E. x E. y ph  <->  E. z E. w [
z  /  x ] [ w  /  y ] ph )
11 equequ2 1737 . . . . . . . . . 10  |-  ( z  =  v  ->  (
x  =  z  <->  x  =  v ) )
12 equequ2 1737 . . . . . . . . . 10  |-  ( w  =  u  ->  (
y  =  w  <->  y  =  u ) )
1311, 12bi2anan9 868 . . . . . . . . 9  |-  ( ( z  =  v  /\  w  =  u )  ->  ( ( x  =  z  /\  y  =  w )  <->  ( x  =  v  /\  y  =  u ) ) )
1413imbi2d 316 . . . . . . . 8  |-  ( ( z  =  v  /\  w  =  u )  ->  ( ( ph  ->  ( x  =  z  /\  y  =  w )
)  <->  ( ph  ->  ( x  =  v  /\  y  =  u )
) ) )
15142albidv 1681 . . . . . . 7  |-  ( ( z  =  v  /\  w  =  u )  ->  ( A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
)  <->  A. x A. y
( ph  ->  ( x  =  v  /\  y  =  u ) ) ) )
1615cbvex2v 1979 . . . . . 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 1673 . . . . . . . . 9  |-  F/ z ( ph  ->  (
x  =  v  /\  y  =  u )
)
18 nfv 1673 . . . . . . . . 9  |-  F/ w
( ph  ->  ( x  =  v  /\  y  =  u ) )
19 nfv 1673 . . . . . . . . . 10  |-  F/ x
( z  =  v  /\  w  =  u )
204, 19nfim 1853 . . . . . . . . 9  |-  F/ x
( [ z  /  x ] [ w  / 
y ] ph  ->  ( z  =  v  /\  w  =  u )
)
21 nfv 1673 . . . . . . . . . 10  |-  F/ y ( z  =  v  /\  w  =  u )
226, 21nfim 1853 . . . . . . . . 9  |-  F/ y ( [ z  /  x ] [ w  / 
y ] ph  ->  ( z  =  v  /\  w  =  u )
)
23 equequ1 1736 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
x  =  v  <->  z  =  v ) )
24 equequ1 1736 . . . . . . . . . . 11  |-  ( y  =  w  ->  (
y  =  u  <->  w  =  u ) )
2523, 24bi2anan9 868 . . . . . . . . . 10  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ( x  =  v  /\  y  =  u )  <->  ( z  =  v  /\  w  =  u ) ) )
269, 25imbi12d 320 . . . . . . . . 9  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ( ph  ->  ( x  =  v  /\  y  =  u )
)  <->  ( [ z  /  x ] [
w  /  y ]
ph  ->  ( z  =  v  /\  w  =  u ) ) ) )
2717, 18, 20, 22, 26cbval2 1975 . . . . . . . 8  |-  ( A. x A. y ( ph  ->  ( x  =  v  /\  y  =  u ) )  <->  A. z A. w ( [ z  /  x ] [
w  /  y ]
ph  ->  ( z  =  v  /\  w  =  u ) ) )
28272exbii 1635 . . . . . . 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 2360 . . . . . . 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 249 . . . . . 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 249 . . . . 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 1652 . . . . 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 479 . . . 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 1666 . . . . . . 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 450 . . . . . . 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 249 . . . . . 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 1635 . . . . 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 1673 . . . . . . . . . . . 12  |-  F/ v ( ( [ z  /  x ] [
w  /  y ]
ph  /\  ph )  -> 
( z  =  x  /\  w  =  y ) )
39 nfv 1673 . . . . . . . . . . . 12  |-  F/ u
( ( [ z  /  x ] [
w  /  y ]
ph  /\  ph )  -> 
( z  =  x  /\  w  =  y ) )
404nfsb 2146 . . . . . . . . . . . . . . 15  |-  F/ x [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
4140nfsb 2146 . . . . . . . . . . . . . 14  |-  F/ x [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
424, 41nfan 1861 . . . . . . . . . . . . 13  |-  F/ x
( [ z  /  x ] [ w  / 
y ] ph  /\  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
4342, 19nfim 1853 . . . . . . . . . . . 12  |-  F/ x
( ( [ z  /  x ] [
w  /  y ]
ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
)
446nfsb 2146 . . . . . . . . . . . . . . 15  |-  F/ y [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
4544nfsb 2146 . . . . . . . . . . . . . 14  |-  F/ y [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph
466, 45nfan 1861 . . . . . . . . . . . . 13  |-  F/ y ( [ z  /  x ] [ w  / 
y ] ph  /\  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
4746, 21nfim 1853 . . . . . . . . . . . 12  |-  F/ y ( ( [ z  /  x ] [
w  /  y ]
ph  /\  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph )  ->  (
z  =  v  /\  w  =  u )
)
48 sbequ12 1936 . . . . . . . . . . . . . . . 16  |-  ( y  =  u  ->  ( ph 
<->  [ u  /  y ] ph ) )
49 sbequ12 1936 . . . . . . . . . . . . . . . 16  |-  ( x  =  v  ->  ( [ u  /  y ] ph  <->  [ v  /  x ] [ u  /  y ] ph ) )
5048, 49sylan9bbr 700 . . . . . . . . . . . . . . 15  |-  ( ( x  =  v  /\  y  =  u )  ->  ( ph  <->  [ v  /  x ] [ u  /  y ] ph ) )
513sbco2 2111 . . . . . . . . . . . . . . . . 17  |-  ( [ u  /  w ] [ w  /  y ] ph  <->  [ u  /  y ] ph )
5251sbbii 1707 . . . . . . . . . . . . . . . 16  |-  ( [ v  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  x ] [ u  /  y ] ph )
53 nfv 1673 . . . . . . . . . . . . . . . . . 18  |-  F/ z [ u  /  w ] [ w  /  y ] ph
5453sbco2 2111 . . . . . . . . . . . . . . . . 17  |-  ( [ v  /  z ] [ z  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  x ] [ u  /  w ] [ w  /  y ] ph )
55 sbcom2 2151 . . . . . . . . . . . . . . . . . 18  |-  ( [ z  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5655sbbii 1707 . . . . . . . . . . . . . . . . 17  |-  ( [ v  /  z ] [ z  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5754, 56bitr3i 251 . . . . . . . . . . . . . . . 16  |-  ( [ v  /  x ] [ u  /  w ] [ w  /  y ] ph  <->  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5852, 57bitr3i 251 . . . . . . . . . . . . . . 15  |-  ( [ v  /  x ] [ u  /  y ] ph  <->  [ v  /  z ] [ u  /  w ] [ z  /  x ] [ w  /  y ] ph )
5950, 58syl6bb 261 . . . . . . . . . . . . . 14  |-  ( ( x  =  v  /\  y  =  u )  ->  ( ph  <->  [ v  /  z ] [
u  /  w ] [ z  /  x ] [ w  /  y ] ph ) )
6059anbi2d 703 . . . . . . . . . . . . 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 1737 . . . . . . . . . . . . . 14  |-  ( x  =  v  ->  (
z  =  x  <->  z  =  v ) )
62 equequ2 1737 . . . . . . . . . . . . . 14  |-  ( y  =  u  ->  (
w  =  y  <->  w  =  u ) )
6361, 62bi2anan9 868 . . . . . . . . . . . . 13  |-  ( ( x  =  v  /\  y  =  u )  ->  ( ( z  =  x  /\  w  =  y )  <->  ( z  =  v  /\  w  =  u ) ) )
6460, 63imbi12d 320 . . . . . . . . . . . 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 1975 . . . . . . . . . . 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 1732 . . . . . . . . . . . . . . 15  |-  ( z  =  x  <->  x  =  z )
67 equcom 1732 . . . . . . . . . . . . . . 15  |-  ( w  =  y  <->  y  =  w )
6866, 67anbi12i 697 . . . . . . . . . . . . . 14  |-  ( ( z  =  x  /\  w  =  y )  <->  ( x  =  z  /\  y  =  w )
)
6968imbi2i 312 . . . . . . . . . . . . 13  |-  ( ( ( [ z  /  x ] [ w  / 
y ] ph  /\  ph )  ->  ( z  =  x  /\  w  =  y ) )  <-> 
( ( [ z  /  x ] [
w  /  y ]
ph  /\  ph )  -> 
( x  =  z  /\  y  =  w ) ) )
70 impexp 446 . . . . . . . . . . . . 13  |-  ( ( ( [ z  /  x ] [ w  / 
y ] ph  /\  ph )  ->  ( x  =  z  /\  y  =  w ) )  <->  ( [
z  /  x ] [ w  /  y ] ph  ->  ( ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
7169, 70bitri 249 . . . . . . . . . . . 12  |-  ( ( ( [ z  /  x ] [ w  / 
y ] ph  /\  ph )  ->  ( z  =  x  /\  w  =  y ) )  <-> 
( [ z  /  x ] [ w  / 
y ] ph  ->  (
ph  ->  ( x  =  z  /\  y  =  w ) ) ) )
72712albii 1611 . . . . . . . . . . 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 251 . . . . . . . . . 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 1886 . . . . . . . . . 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 249 . . . . . . . . 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 694 . . . . . . . 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 793 . . . . . . . 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 252 . . . . . . 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 2150 . . . . . . . 8  |-  ( [ z  /  x ] [ w  /  y ] ph  <->  A. x A. y
( ( x  =  z  /\  y  =  w )  ->  ph )
)
8079anbi1i 695 . . . . . . 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 249 . . . . . 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 1635 . . . . 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 252 . . . 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 212 . . 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 198 . . . . . . 7  |-  ( (
ph 
<->  ( x  =  z  /\  y  =  w ) )  ->  (
( x  =  z  /\  y  =  w )  ->  ph ) )
86852alimi 1605 . . . . . 6  |-  ( A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  ->  A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph )
)
87862eximi 1626 . . . . 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 2182 . . . . 5  |-  ( E. x E. y ph  <->  E. z E. w A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph ) )
8987, 88sylibr 212 . . . 4  |-  ( E. z E. w A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  ->  E. x E. y ph )
90 bi1 186 . . . . . 6  |-  ( (
ph 
<->  ( x  =  z  /\  y  =  w ) )  ->  ( ph  ->  ( x  =  z  /\  y  =  w ) ) )
91902alimi 1605 . . . . 5  |-  ( A. x A. y ( ph  <->  ( x  =  z  /\  y  =  w )
)  ->  A. x A. y ( ph  ->  ( x  =  z  /\  y  =  w )
) )
92912eximi 1626 . . . 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 532 . . 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 188 . 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 249 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 setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1367   E.wex 1586   [wsb 1700   E!weu 2253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator