Theorem fvmptg

Description: Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007) (Revised by Mario Carneiro, 31-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		fvmptg.1	$$⊢x=A\to B=C$$
2		fvmptg.2	$$⊢F=\left(x\in D⟼B\right)$$
3		eqid	$$⊢C=C$$
4	1	eqeq2d	$$⊢x=A\to \left(y=B\leftrightarrow y=C\right)$$
5		eqeq1	$$⊢y=C\to \left(y=C\leftrightarrow C=C\right)$$
6		moeq	$$⊢{\exists }^{*}yy=B$$
7	6	a1i	$$⊢x\in D\to {\exists }^{*}yy=B$$
8		df-mpt	$$⊢\left(x\in D⟼B\right)=\left\{⟨x,y⟩|\left(x\in D\wedge y=B\right)\right\}$$
9	2 8	eqtri	$$⊢F=\left\{⟨x,y⟩|\left(x\in D\wedge y=B\right)\right\}$$
10	4 5 7 9	fvopab3ig	$$⊢\left(A\in D\wedge C\in R\right)\to \left(C=C\to F\left(A\right)=C\right)$$
11	3 10	mpi	$$⊢\left(A\in D\wedge C\in R\right)\to F\left(A\right)=C$$