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

Proof

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