Step |
Hyp |
Ref |
Expression |
1 |
|
equsb1 |
|- [ y / x ] x = y |
2 |
|
sban |
|- ( [ y / x ] ( x = y /\ ph ) <-> ( [ y / x ] x = y /\ [ y / x ] ph ) ) |
3 |
2
|
simplbi2com |
|- ( [ y / x ] ph -> ( [ y / x ] x = y -> [ y / x ] ( x = y /\ ph ) ) ) |
4 |
1 3
|
mpi |
|- ( [ y / x ] ph -> [ y / x ] ( x = y /\ ph ) ) |
5 |
|
spsbe |
|- ( [ y / x ] ( x = y /\ ph ) -> E. x ( x = y /\ ph ) ) |
6 |
4 5
|
syl |
|- ( [ y / x ] ph -> E. x ( x = y /\ ph ) ) |
7 |
|
hbs1 |
|- ( [ y / x ] ph -> A. x [ y / x ] ph ) |
8 |
|
simpr |
|- ( ( x = y /\ ph ) -> ph ) |
9 |
8
|
a1i |
|- ( E. x ( x = y /\ ph ) -> ( ( x = y /\ ph ) -> ph ) ) |
10 |
|
simpl |
|- ( ( x = y /\ ph ) -> x = y ) |
11 |
10
|
a1i |
|- ( E. x ( x = y /\ ph ) -> ( ( x = y /\ ph ) -> x = y ) ) |
12 |
|
sbequ1 |
|- ( x = y -> ( ph -> [ y / x ] ph ) ) |
13 |
12
|
com12 |
|- ( ph -> ( x = y -> [ y / x ] ph ) ) |
14 |
9 11 13
|
syl6c |
|- ( E. x ( x = y /\ ph ) -> ( ( x = y /\ ph ) -> [ y / x ] ph ) ) |
15 |
7 14
|
exlimexi |
|- ( E. x ( x = y /\ ph ) -> [ y / x ] ph ) |
16 |
6 15
|
impbii |
|- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) ) |