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

Metamath Proof Explorer

Theorem fmpt3d

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017)

Ref Expression
Hypotheses fmpt3d.1 ⊢ φ → F = x ∈ A ⟼ B
fmpt3d.2 ⊢ φ ∧ x ∈ A → B ∈ C
Assertion fmpt3d ⊢ φ → F : A ⟶ C

Proof

Step Hyp Ref Expression
1 fmpt3d.1 ⊢ φ → F = x ∈ A ⟼ B
2 fmpt3d.2 ⊢ φ ∧ x ∈ A → B ∈ C
3 2 fmpttd ⊢ φ → x ∈ A ⟼ B : A ⟶ C
4 1 feq1d ⊢ φ → F : A ⟶ C ↔ x ∈ A ⟼ B : A ⟶ C
5 3 4 mpbird ⊢ φ → F : A ⟶ C