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

Metamath Proof Explorer

Theorem fmptd

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013)

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

Proof

Step Hyp Ref Expression
1 fmptd.1 ⊢ φ ∧ x ∈ A → B ∈ C
2 fmptd.2 ⊢ F = x ∈ A ⟼ B
3 1 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ C
4 2 fmpt ⊢ ∀ x ∈ A B ∈ C ↔ F : A ⟶ C
5 3 4 sylib ⊢ φ → F : A ⟶ C