Theorem fmpti

Description: Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005) (Revised by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Hypotheses	fmpt.1	$$⊢F=\left(x\in A⟼C\right)$$
	fmpti.2	$$⊢x\in A\to C\in B$$
Assertion	fmpti	$$⊢F:A⟶B$$

Proof

Step	Hyp	Ref	Expression
1		fmpt.1	$$⊢F=\left(x\in A⟼C\right)$$
2		fmpti.2	$$⊢x\in A\to C\in B$$
3	2	rgen	$$⊢\forall x\in AC\in B$$
4	1	fmpt	$$⊢\forall x\in AC\in B\leftrightarrow F:A⟶B$$
5	3 4	mpbi	$$⊢F:A⟶B$$