Theorem fvmptd3

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

	Ref	Expression
Hypotheses	fvmptd3.1	$$⊢F=\left(x\in D⟼B\right)$$
	fvmptd3.2	$$⊢x=A\to B=C$$
	fvmptd3.3	$$⊢\phi \to A\in D$$
	fvmptd3.4	$$⊢\phi \to C\in V$$
Assertion	fvmptd3	$$⊢\phi \to F\left(A\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		fvmptd3.1	$$⊢F=\left(x\in D⟼B\right)$$
2		fvmptd3.2	$$⊢x=A\to B=C$$
3		fvmptd3.3	$$⊢\phi \to A\in D$$
4		fvmptd3.4	$$⊢\phi \to C\in V$$
5	2 1	fvmptg	$$⊢\left(A\in D\wedge C\in V\right)\to F\left(A\right)=C$$
6	3 4 5	syl2anc	$$⊢\phi \to F\left(A\right)=C$$