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

Metamath Proof Explorer

Theorem fnmpt

Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013)

Ref Expression
Hypothesis mptfng.1 ⊢ F = x ∈ A ⟼ B
Assertion fnmpt ⊢ ∀ x ∈ A B ∈ V → F Fn A

Proof

Step Hyp Ref Expression
1 mptfng.1 ⊢ F = x ∈ A ⟼ B
2 elex ⊢ B ∈ V → B ∈ V
3 2 ralimi ⊢ ∀ x ∈ A B ∈ V → ∀ x ∈ A B ∈ V
4 1 mptfng ⊢ ∀ x ∈ A B ∈ V ↔ F Fn A
5 3 4 sylib ⊢ ∀ x ∈ A B ∈ V → F Fn A