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

Metamath Proof Explorer

Theorem fnmptf

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
Hypothesis mptfnf.0 ⊢ Ⅎ _ x A
Assertion fnmptf ⊢ ∀ x ∈ A B ∈ V → x ∈ A ⟼ B Fn A

Proof

Step Hyp Ref Expression
1 mptfnf.0 ⊢ Ⅎ _ x A
2 elex ⊢ B ∈ V → B ∈ V
3 2 ralimi ⊢ ∀ x ∈ A B ∈ V → ∀ x ∈ A B ∈ V
4 1 mptfnf ⊢ ∀ x ∈ A B ∈ V ↔ x ∈ A ⟼ B Fn A
5 3 4 sylib ⊢ ∀ x ∈ A B ∈ V → x ∈ A ⟼ B Fn A