This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝐹 : 𝐴 ⟶ 𝐵