Theorem fvmpt3i

Description: Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	fvmpt3.a	$$⊢x=A\to B=C$$
	fvmpt3.b	$$⊢F=\left(x\in D⟼B\right)$$
	fvmpt3i.c	$$⊢B\in \mathrm{V}$$
Assertion	fvmpt3i	$$⊢A\in D\to F\left(A\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		fvmpt3.a	$$⊢x=A\to B=C$$
2		fvmpt3.b	$$⊢F=\left(x\in D⟼B\right)$$
3		fvmpt3i.c	$$⊢B\in \mathrm{V}$$
4	3	a1i	$$⊢x\in D\to B\in \mathrm{V}$$
5	1 2 4	fvmpt3	$$⊢A\in D\to F\left(A\right)=C$$