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

Metamath Proof Explorer

Theorem fnmptif

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Hypotheses fnmptif.1 ⊢ Ⅎ 𝑥 𝐴
fnmptif.2 ⊢ 𝐵 ∈ V
fnmptif.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion fnmptif 𝐹 Fn 𝐴

Proof

Step Hyp Ref Expression
1 fnmptif.1 ⊢ Ⅎ 𝑥 𝐴
2 fnmptif.2 ⊢ 𝐵 ∈ V
3 fnmptif.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4 2 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V
5 1 mptfnf ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
6 4 5 mpbi ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴
7 3 fneq1i ⊢ ( 𝐹 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
8 6 7 mpbir ⊢ 𝐹 Fn 𝐴