Metamath Proof Explorer

Theorem fvmptdf

Description: Deduction version of fvmptd using bound-variable hypotheses instead of distinct variable conditions. (Contributed by AV, 29-Mar-2024)

Ref Expression
Hypotheses fvmptd.1 
|- ( ph -> F = ( x e. D |-> B ) )
fvmptd.2 
|- ( ( ph /\ x = A ) -> B = C )
fvmptd.3 
|- ( ph -> A e. D )
fvmptd.4 
|- ( ph -> C e. V )
fvmptdf.p 
|- F/ x ph
fvmptdf.a 
|- F/_ x A
fvmptdf.c 
|- F/_ x C
Assertion fvmptdf 
|- ( ph -> ( F ` A ) = C )

Proof

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 )