Step |
Hyp |
Ref |
Expression |
1 |
|
csbeq1 |
|- ( w = A -> [_ w / x ]_ { <. y , z >. | ph } = [_ A / x ]_ { <. y , z >. | ph } ) |
2 |
|
dfsbcq2 |
|- ( w = A -> ( [ w / x ] ph <-> [. A / x ]. ph ) ) |
3 |
2
|
opabbidv |
|- ( w = A -> { <. y , z >. | [ w / x ] ph } = { <. y , z >. | [. A / x ]. ph } ) |
4 |
1 3
|
eqeq12d |
|- ( w = A -> ( [_ w / x ]_ { <. y , z >. | ph } = { <. y , z >. | [ w / x ] ph } <-> [_ A / x ]_ { <. y , z >. | ph } = { <. y , z >. | [. A / x ]. ph } ) ) |
5 |
|
vex |
|- w e. _V |
6 |
|
nfs1v |
|- F/ x [ w / x ] ph |
7 |
6
|
nfopab |
|- F/_ x { <. y , z >. | [ w / x ] ph } |
8 |
|
sbequ12 |
|- ( x = w -> ( ph <-> [ w / x ] ph ) ) |
9 |
8
|
opabbidv |
|- ( x = w -> { <. y , z >. | ph } = { <. y , z >. | [ w / x ] ph } ) |
10 |
5 7 9
|
csbief |
|- [_ w / x ]_ { <. y , z >. | ph } = { <. y , z >. | [ w / x ] ph } |
11 |
4 10
|
vtoclg |
|- ( A e. _V -> [_ A / x ]_ { <. y , z >. | ph } = { <. y , z >. | [. A / x ]. ph } ) |
12 |
|
csbprc |
|- ( -. A e. _V -> [_ A / x ]_ { <. y , z >. | ph } = (/) ) |
13 |
|
sbcex |
|- ( [. A / x ]. ph -> A e. _V ) |
14 |
13
|
con3i |
|- ( -. A e. _V -> -. [. A / x ]. ph ) |
15 |
14
|
nexdv |
|- ( -. A e. _V -> -. E. z [. A / x ]. ph ) |
16 |
15
|
nexdv |
|- ( -. A e. _V -> -. E. y E. z [. A / x ]. ph ) |
17 |
|
opabn0 |
|- ( { <. y , z >. | [. A / x ]. ph } =/= (/) <-> E. y E. z [. A / x ]. ph ) |
18 |
17
|
necon1bbii |
|- ( -. E. y E. z [. A / x ]. ph <-> { <. y , z >. | [. A / x ]. ph } = (/) ) |
19 |
16 18
|
sylib |
|- ( -. A e. _V -> { <. y , z >. | [. A / x ]. ph } = (/) ) |
20 |
12 19
|
eqtr4d |
|- ( -. A e. _V -> [_ A / x ]_ { <. y , z >. | ph } = { <. y , z >. | [. A / x ]. ph } ) |
21 |
11 20
|
pm2.61i |
|- [_ A / x ]_ { <. y , z >. | ph } = { <. y , z >. | [. A / x ]. ph } |