Theorem fvmpt2

Description: Value of a function given by the maps-to notation. (Contributed by FL, 21-Jun-2010)

	Ref	Expression
Hypothesis	mptrcl.1	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	fvmpt2	$$⊢\left(x\in A\wedge B\in C\right)\to F\left(x\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		mptrcl.1	$$⊢F=\left(x\in A⟼B\right)$$
2	1	fvmpt2i	$$⊢x\in A\to F\left(x\right)=\mathrm{I}\left(B\right)$$
3		fvi	$$⊢B\in C\to \mathrm{I}\left(B\right)=B$$
4	2 3	sylan9eq	$$⊢\left(x\in A\wedge B\in C\right)\to F\left(x\right)=B$$