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

Metamath Proof Explorer

Theorem fnmptd

Description: The maps-to notation defines a function with domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 fnmptd.1 ⊢ Ⅎ x φ
2 fnmptd.2 ⊢ φ ∧ x ∈ A → B ∈ V
3 fnmptd.3 ⊢ F = x ∈ A ⟼ B
4 2 ex ⊢ φ → x ∈ A → B ∈ V
5 1 4 ralrimi ⊢ φ → ∀ x ∈ A B ∈ V
6 3 fnmpt ⊢ ∀ x ∈ A B ∈ V → F Fn A
7 5 6 syl ⊢ φ → F Fn A