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 ⊢ F = x ∈ A ⟼ C
fmpti.2 ⊢ x ∈ A → C ∈ B
Assertion fmpti ⊢ F : A ⟶ B

Proof

Step Hyp Ref Expression
1 fmpt.1 ⊢ F = x ∈ A ⟼ C
2 fmpti.2 ⊢ x ∈ A → C ∈ B
3 2 rgen ⊢ ∀ x ∈ A C ∈ B
4 1 fmpt ⊢ ∀ x ∈ A C ∈ B ↔ F : A ⟶ B
5 3 4 mpbi ⊢ F : A ⟶ B