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 ⊢ Ⅎ _ x A
fnmptif.2 ⊢ B ∈ V
fnmptif.3 ⊢ F = x ∈ A ⟼ B
Assertion fnmptif ⊢ F Fn A

Proof

Step Hyp Ref Expression
1 fnmptif.1 ⊢ Ⅎ _ x A
2 fnmptif.2 ⊢ B ∈ V
3 fnmptif.3 ⊢ F = x ∈ A ⟼ B
4 2 rgenw ⊢ ∀ x ∈ A B ∈ V
5 1 mptfnf ⊢ ∀ x ∈ A B ∈ V ↔ x ∈ A ⟼ B Fn A
6 4 5 mpbi ⊢ x ∈ A ⟼ B Fn A
7 3 fneq1i ⊢ F Fn A ↔ x ∈ A ⟼ B Fn A
8 6 7 mpbir ⊢ F Fn A