This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ φ \to F = (x \in D ⟼ B)$
	fvmptd.2	$⊢ (φ \land x = A) \to B = C$
	fvmptd.3	$⊢ φ \to A \in D$
	fvmptd.4	$⊢ φ \to C \in V$
Assertion	fvmptd	$⊢ φ \to F (A) = C$

Proof

Step	Hyp	Ref	Expression
1		fvmptd.1	$⊢ φ \to F = (x \in D ⟼ B)$
2		fvmptd.2	$⊢ (φ \land x = A) \to B = C$
3		fvmptd.3	$⊢ φ \to A \in D$
4		fvmptd.4	$⊢ φ \to C \in V$
5		nfv	$⊢ Ⅎ x φ$
6		nfcv	$⊢ \underline{Ⅎ} x A$
7		nfcv	$⊢ \underline{Ⅎ} x C$
8	1 2 3 4 5 6 7	fvmptdf	$⊢ φ \to F (A) = C$