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

Metamath Proof Explorer

Theorem fmpt2d

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014)

Ref Expression
Hypotheses fmpt2d.2 ⊢ φ ∧ x ∈ A → B ∈ V
fmpt2d.1 ⊢ φ → F = x ∈ A ⟼ B
fmpt2d.3 ⊢ φ ∧ y ∈ A → F ⁡ y ∈ C
Assertion fmpt2d ⊢ φ → F : A ⟶ C

Proof

Step Hyp Ref Expression
1 fmpt2d.2 ⊢ φ ∧ x ∈ A → B ∈ V
2 fmpt2d.1 ⊢ φ → F = x ∈ A ⟼ B
3 fmpt2d.3 ⊢ φ ∧ y ∈ A → F ⁡ y ∈ C
4 1 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ V
5 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
6 5 fnmpt ⊢ ∀ x ∈ A B ∈ V → x ∈ A ⟼ B Fn A
7 4 6 syl ⊢ φ → x ∈ A ⟼ B Fn A
8 2 fneq1d ⊢ φ → F Fn A ↔ x ∈ A ⟼ B Fn A
9 7 8 mpbird ⊢ φ → F Fn A
10 3 ralrimiva ⊢ φ → ∀ y ∈ A F ⁡ y ∈ C
11 ffnfv ⊢ F : A ⟶ C ↔ F Fn A ∧ ∀ y ∈ A F ⁡ y ∈ C
12 9 10 11 sylanbrc ⊢ φ → F : A ⟶ C