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

Metamath Proof Explorer

Theorem fnmpti

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses fnmpti.1 ⊢ B ∈ V
fnmpti.2 ⊢ F = x ∈ A ⟼ B
Assertion fnmpti ⊢ F Fn A

Proof

Step Hyp Ref Expression
1 fnmpti.1 ⊢ B ∈ V
2 fnmpti.2 ⊢ F = x ∈ A ⟼ B
3 1 rgenw ⊢ ∀ x ∈ A B ∈ V
4 2 mptfng ⊢ ∀ x ∈ A B ∈ V ↔ F Fn A
5 3 4 mpbi ⊢ F Fn A