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

Metamath Proof Explorer

Theorem fnopab

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 5-Mar-1996)

Ref Expression
Hypotheses fnopab.1 ⊢ x ∈ A → ∃! y φ
fnopab.2 ⊢ F = x y | x ∈ A ∧ φ
Assertion fnopab ⊢ F Fn A

Proof

Step Hyp Ref Expression
1 fnopab.1 ⊢ x ∈ A → ∃! y φ
2 fnopab.2 ⊢ F = x y | x ∈ A ∧ φ
3 1 rgen ⊢ ∀ x ∈ A ∃! y φ
4 2 fnopabg ⊢ ∀ x ∈ A ∃! y φ ↔ F Fn A
5 3 4 mpbi ⊢ F Fn A