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

Metamath Proof Explorer

Theorem mptfnd

Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013) (Revised by Thierry Arnoux, 10-May-2017)

Ref Expression
Hypotheses mptfnd.1 ⊢ Ⅎ _ x A
mptfnd.2 ⊢ Ⅎ x φ
mptfnd.3 ⊢ φ ∧ x ∈ A → B ∈ V
Assertion mptfnd ⊢ φ → x ∈ A ⟼ B Fn A

Proof

Step Hyp Ref Expression
1 mptfnd.1 ⊢ Ⅎ _ x A
2 mptfnd.2 ⊢ Ⅎ x φ
3 mptfnd.3 ⊢ φ ∧ x ∈ A → B ∈ V
4 3 ex ⊢ φ → x ∈ A → B ∈ V
5 elex ⊢ B ∈ V → B ∈ V
6 4 5 syl6 ⊢ φ → x ∈ A → B ∈ V
7 2 6 ralrimi ⊢ φ → ∀ x ∈ A B ∈ V
8 1 mptfnf ⊢ ∀ x ∈ A B ∈ V ↔ x ∈ A ⟼ B Fn A
9 7 8 sylib ⊢ φ → x ∈ A ⟼ B Fn A