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 )