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

Metamath Proof Explorer

Theorem fnopabg

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004) (Proof shortened by Mario Carneiro, 4-Dec-2016)

Ref Expression
Hypothesis fnopabg.1 ⊢ F = x y | x ∈ A ∧ φ
Assertion fnopabg ⊢ ∀ x ∈ A ∃! y φ ↔ F Fn A

Proof

Step Hyp Ref Expression
1 fnopabg.1 ⊢ F = x y | x ∈ A ∧ φ
2 moanimv ⊢ ∃* y x ∈ A ∧ φ ↔ x ∈ A → ∃* y φ
3 2 albii ⊢ ∀ x ∃* y x ∈ A ∧ φ ↔ ∀ x x ∈ A → ∃* y φ
4 funopab ⊢ Fun ⁡ x y | x ∈ A ∧ φ ↔ ∀ x ∃* y x ∈ A ∧ φ
5 df-ral ⊢ ∀ x ∈ A ∃* y φ ↔ ∀ x x ∈ A → ∃* y φ
6 3 4 5 3bitr4ri ⊢ ∀ x ∈ A ∃* y φ ↔ Fun ⁡ x y | x ∈ A ∧ φ
7 dmopab3 ⊢ ∀ x ∈ A ∃ y φ ↔ dom ⁡ x y | x ∈ A ∧ φ = A
8 6 7 anbi12i ⊢ ∀ x ∈ A ∃* y φ ∧ ∀ x ∈ A ∃ y φ ↔ Fun ⁡ x y | x ∈ A ∧ φ ∧ dom ⁡ x y | x ∈ A ∧ φ = A
9 r19.26 ⊢ ∀ x ∈ A ∃* y φ ∧ ∃ y φ ↔ ∀ x ∈ A ∃* y φ ∧ ∀ x ∈ A ∃ y φ
10 df-fn ⊢ x y | x ∈ A ∧ φ Fn A ↔ Fun ⁡ x y | x ∈ A ∧ φ ∧ dom ⁡ x y | x ∈ A ∧ φ = A
11 8 9 10 3bitr4i ⊢ ∀ x ∈ A ∃* y φ ∧ ∃ y φ ↔ x y | x ∈ A ∧ φ Fn A
12 df-eu ⊢ ∃! y φ ↔ ∃ y φ ∧ ∃* y φ
13 12 biancomi ⊢ ∃! y φ ↔ ∃* y φ ∧ ∃ y φ
14 13 ralbii ⊢ ∀ x ∈ A ∃! y φ ↔ ∀ x ∈ A ∃* y φ ∧ ∃ y φ
15 1 fneq1i ⊢ F Fn A ↔ x y | x ∈ A ∧ φ Fn A
16 11 14 15 3bitr4i ⊢ ∀ x ∈ A ∃! y φ ↔ F Fn A