Metamath Proof Explorer


Theorem fvmptd

Description: Deduction version of fvmpt . (Contributed by Scott Fenton, 18-Feb-2013) (Revised by Mario Carneiro, 31-Aug-2015) (Proof shortened by AV, 29-Mar-2024)

Ref Expression
Hypotheses fvmptd.1 φF=xDB
fvmptd.2 φx=AB=C
fvmptd.3 φAD
fvmptd.4 φCV
Assertion fvmptd φFA=C

Proof

Step Hyp Ref Expression
1 fvmptd.1 φF=xDB
2 fvmptd.2 φx=AB=C
3 fvmptd.3 φAD
4 fvmptd.4 φCV
5 nfv xφ
6 nfcv _xA
7 nfcv _xC
8 1 2 3 4 5 6 7 fvmptdf φFA=C