Step |
Hyp |
Ref |
Expression |
1 |
|
fvmptd.1 |
|- ( ph -> F = ( x e. D |-> B ) ) |
2 |
|
fvmptd.2 |
|- ( ( ph /\ x = A ) -> B = C ) |
3 |
|
fvmptd.3 |
|- ( ph -> A e. D ) |
4 |
|
fvmptd.4 |
|- ( ph -> C e. V ) |
5 |
|
fvmptdf.p |
|- F/ x ph |
6 |
|
fvmptdf.a |
|- F/_ x A |
7 |
|
fvmptdf.c |
|- F/_ x C |
8 |
1
|
fveq1d |
|- ( ph -> ( F ` A ) = ( ( x e. D |-> B ) ` A ) ) |
9 |
|
nfcsb1v |
|- F/_ x [_ y / x ]_ B |
10 |
9
|
a1i |
|- ( ph -> F/_ x [_ y / x ]_ B ) |
11 |
7
|
a1i |
|- ( ph -> F/_ x C ) |
12 |
|
csbeq1a |
|- ( x = y -> B = [_ y / x ]_ B ) |
13 |
12
|
adantl |
|- ( ( ph /\ x = y ) -> B = [_ y / x ]_ B ) |
14 |
6
|
nfeq2 |
|- F/ x y = A |
15 |
5 14
|
nfan |
|- F/ x ( ph /\ y = A ) |
16 |
7
|
a1i |
|- ( ( ph /\ y = A ) -> F/_ x C ) |
17 |
|
vex |
|- y e. _V |
18 |
17
|
a1i |
|- ( ( ph /\ y = A ) -> y e. _V ) |
19 |
|
eqtr |
|- ( ( x = y /\ y = A ) -> x = A ) |
20 |
19
|
ancoms |
|- ( ( y = A /\ x = y ) -> x = A ) |
21 |
20 2
|
sylan2 |
|- ( ( ph /\ ( y = A /\ x = y ) ) -> B = C ) |
22 |
21
|
anassrs |
|- ( ( ( ph /\ y = A ) /\ x = y ) -> B = C ) |
23 |
15 16 18 22
|
csbiedf |
|- ( ( ph /\ y = A ) -> [_ y / x ]_ B = C ) |
24 |
5 10 11 3 13 23
|
csbie2df |
|- ( ph -> [_ A / x ]_ B = C ) |
25 |
24 4
|
eqeltrd |
|- ( ph -> [_ A / x ]_ B e. V ) |
26 |
|
eqid |
|- ( x e. D |-> B ) = ( x e. D |-> B ) |
27 |
26
|
fvmpts |
|- ( ( A e. D /\ [_ A / x ]_ B e. V ) -> ( ( x e. D |-> B ) ` A ) = [_ A / x ]_ B ) |
28 |
3 25 27
|
syl2anc |
|- ( ph -> ( ( x e. D |-> B ) ` A ) = [_ A / x ]_ B ) |
29 |
8 28 24
|
3eqtrd |
|- ( ph -> ( F ` A ) = C ) |