Metamath Proof Explorer


Theorem fvmptd3

Description: Deduction version of fvmpt . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

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