Metamath Proof Explorer


Theorem fvmptd4

Description: Deduction version of fvmpt (where the substitution hypothesis does not have the antecedent ph ). (Contributed by SN, 26-Jul-2024)

Ref Expression
Hypotheses fvmptd4.1
|- ( x = A -> B = C )
fvmptd4.2
|- ( ph -> F = ( x e. D |-> B ) )
fvmptd4.3
|- ( ph -> A e. D )
fvmptd4.4
|- ( ph -> C e. V )
Assertion fvmptd4
|- ( ph -> ( F ` A ) = C )

Proof

Step Hyp Ref Expression
1 fvmptd4.1
 |-  ( x = A -> B = C )
2 fvmptd4.2
 |-  ( ph -> F = ( x e. D |-> B ) )
3 fvmptd4.3
 |-  ( ph -> A e. D )
4 fvmptd4.4
 |-  ( ph -> C e. V )
5 1 adantl
 |-  ( ( ph /\ x = A ) -> B = C )
6 2 5 3 4 fvmptd
 |-  ( ph -> ( F ` A ) = C )