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	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
	fmpti.2	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 )
Assertion	fmpti	⊢ 𝐹 : 𝐴 ⟶ 𝐵

Proof

Step	Hyp	Ref	Expression
1		fmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
2		fmpti.2	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 )
3	2	rgen	⊢ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵
4	1	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )
5	3 4	mpbi	⊢ 𝐹 : 𝐴 ⟶ 𝐵