Step |
Hyp |
Ref |
Expression |
1 |
|
nfcv |
|- F/_ x (/) |
2 |
|
df-csb |
|- [_ A / x ]_ (/) = { y | [. A / x ]. y e. (/) } |
3 |
|
dfsbcq2 |
|- ( z = A -> ( [ z / x ] y e. (/) <-> [. A / x ]. y e. (/) ) ) |
4 |
3
|
bibi1d |
|- ( z = A -> ( ( [ z / x ] y e. (/) <-> y e. (/) ) <-> ( [. A / x ]. y e. (/) <-> y e. (/) ) ) ) |
5 |
4
|
imbi2d |
|- ( z = A -> ( ( F/ x y e. (/) -> ( [ z / x ] y e. (/) <-> y e. (/) ) ) <-> ( F/ x y e. (/) -> ( [. A / x ]. y e. (/) <-> y e. (/) ) ) ) ) |
6 |
|
sbv |
|- ( [ z / x ] y e. (/) <-> y e. (/) ) |
7 |
6
|
a1i |
|- ( F/ x y e. (/) -> ( [ z / x ] y e. (/) <-> y e. (/) ) ) |
8 |
5 7
|
vtoclg |
|- ( A e. _V -> ( F/ x y e. (/) -> ( [. A / x ]. y e. (/) <-> y e. (/) ) ) ) |
9 |
|
nfcr |
|- ( F/_ x (/) -> F/ x y e. (/) ) |
10 |
8 9
|
impel |
|- ( ( A e. _V /\ F/_ x (/) ) -> ( [. A / x ]. y e. (/) <-> y e. (/) ) ) |
11 |
10
|
abbi1dv |
|- ( ( A e. _V /\ F/_ x (/) ) -> { y | [. A / x ]. y e. (/) } = (/) ) |
12 |
2 11
|
syl5eq |
|- ( ( A e. _V /\ F/_ x (/) ) -> [_ A / x ]_ (/) = (/) ) |
13 |
1 12
|
mpan2 |
|- ( A e. _V -> [_ A / x ]_ (/) = (/) ) |
14 |
|
csbprc |
|- ( -. A e. _V -> [_ A / x ]_ (/) = (/) ) |
15 |
13 14
|
pm2.61i |
|- [_ A / x ]_ (/) = (/) |