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 ⊢ Ⅎ 𝑥 𝐴
Assertion fnmptf ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )

Proof

Step Hyp Ref Expression
1 mptfnf.0 ⊢ Ⅎ 𝑥 𝐴
2 elex ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V )
3 2 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
4 1 mptfnf ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
5 3 4 sylib ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )