Theorem fvmptdv2

Description: Alternate deduction version of fvmpt , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		fvmptdv2.1	$$⊢\phi \to A\in D$$
2		fvmptdv2.2	$$⊢\left(\phi \wedge x=A\right)\to B\in V$$
3		fvmptdv2.3	$$⊢\left(\phi \wedge x=A\right)\to B=C$$
4		eqidd	$$⊢\phi \to \left(x\in D⟼B\right)=\left(x\in D⟼B\right)$$
5	1	elexd	$$⊢\phi \to A\in \mathrm{V}$$
6		isset	$$⊢A\in \mathrm{V}\leftrightarrow \exists xx=A$$
7	5 6	sylib	$$⊢\phi \to \exists xx=A$$
8	2	elexd	$$⊢\left(\phi \wedge x=A\right)\to B\in \mathrm{V}$$
9	3 8	eqeltrrd	$$⊢\left(\phi \wedge x=A\right)\to C\in \mathrm{V}$$
10	7 9	exlimddv	$$⊢\phi \to C\in \mathrm{V}$$
11	4 3 1 10	fvmptd	$$⊢\phi \to \left(x\in D⟼B\right)\left(A\right)=C$$
12		fveq1	$$⊢F=\left(x\in D⟼B\right)\to F\left(A\right)=\left(x\in D⟼B\right)\left(A\right)$$
13	12	eqeq1d	$$⊢F=\left(x\in D⟼B\right)\to \left(F\left(A\right)=C\leftrightarrow \left(x\in D⟼B\right)\left(A\right)=C\right)$$
14	11 13	syl5ibrcom	$$⊢\phi \to \left(F=\left(x\in D⟼B\right)\to F\left(A\right)=C\right)$$