Step |
Hyp |
Ref |
Expression |
1 |
|
nfv |
|- F/ x ( <. A , B >. = <. a , b >. /\ ph ) |
2 |
|
nfv |
|- F/ y ( <. A , B >. = <. a , b >. /\ ph ) |
3 |
|
nfv |
|- F/ a <. A , B >. = <. x , y >. |
4 |
|
nfcv |
|- F/_ a y |
5 |
|
nfsbc1v |
|- F/ a [. x / a ]. ph |
6 |
4 5
|
nfsbcw |
|- F/ a [. y / b ]. [. x / a ]. ph |
7 |
3 6
|
nfan |
|- F/ a ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) |
8 |
|
nfv |
|- F/ b <. A , B >. = <. x , y >. |
9 |
|
nfsbc1v |
|- F/ b [. y / b ]. [. x / a ]. ph |
10 |
8 9
|
nfan |
|- F/ b ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) |
11 |
|
opeq12 |
|- ( ( a = x /\ b = y ) -> <. a , b >. = <. x , y >. ) |
12 |
11
|
eqeq2d |
|- ( ( a = x /\ b = y ) -> ( <. A , B >. = <. a , b >. <-> <. A , B >. = <. x , y >. ) ) |
13 |
|
sbceq1a |
|- ( a = x -> ( ph <-> [. x / a ]. ph ) ) |
14 |
|
sbceq1a |
|- ( b = y -> ( [. x / a ]. ph <-> [. y / b ]. [. x / a ]. ph ) ) |
15 |
13 14
|
sylan9bb |
|- ( ( a = x /\ b = y ) -> ( ph <-> [. y / b ]. [. x / a ]. ph ) ) |
16 |
12 15
|
anbi12d |
|- ( ( a = x /\ b = y ) -> ( ( <. A , B >. = <. a , b >. /\ ph ) <-> ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) ) |
17 |
1 2 7 10 16
|
cbvex2v |
|- ( E. a E. b ( <. A , B >. = <. a , b >. /\ ph ) <-> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) |