Theorem fvmpt3

Description: Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	fvmpt3.a	$$⊢x=A\to B=C$$
	fvmpt3.b	$$⊢F=\left(x\in D⟼B\right)$$
	fvmpt3.c	$$⊢x\in D\to B\in V$$
Assertion	fvmpt3	$$⊢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		fvmpt3.c	$$⊢x\in D\to B\in V$$
4	1	eleq1d	$$⊢x=A\to \left(B\in V\leftrightarrow C\in V\right)$$
5	4 3	vtoclga	$$⊢A\in D\to C\in V$$
6	1 2	fvmptg	$$⊢\left(A\in D\wedge C\in V\right)\to F\left(A\right)=C$$
7	5 6	mpdan	$$⊢A\in D\to F\left(A\right)=C$$