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

Metamath Proof Explorer

Theorem eusv2nf

Description: Two ways to express single-valuedness of a class expression A ( x ) . (Contributed by Mario Carneiro, 18-Nov-2016)

Ref Expression
Hypothesis eusv2.1 ⊢ A ∈ V
Assertion eusv2nf ⊢ ∃! y ∃ x y = A ↔ Ⅎ _ x A

Proof

Step Hyp Ref Expression
1 eusv2.1 ⊢ A ∈ V
2 nfeu1 ⊢ Ⅎ y ∃! y ∃ x y = A
3 nfe1 ⊢ Ⅎ x ∃ x y = A
4 3 nfeuw ⊢ Ⅎ x ∃! y ∃ x y = A
5 1 isseti ⊢ ∃ y y = A
6 19.8a ⊢ y = A → ∃ x y = A
7 6 ancri ⊢ y = A → ∃ x y = A ∧ y = A
8 5 7 eximii ⊢ ∃ y ∃ x y = A ∧ y = A
9 eupick ⊢ ∃! y ∃ x y = A ∧ ∃ y ∃ x y = A ∧ y = A → ∃ x y = A → y = A
10 8 9 mpan2 ⊢ ∃! y ∃ x y = A → ∃ x y = A → y = A
11 4 10 alrimi ⊢ ∃! y ∃ x y = A → ∀ x ∃ x y = A → y = A
12 nf6 ⊢ Ⅎ x y = A ↔ ∀ x ∃ x y = A → y = A
13 11 12 sylibr ⊢ ∃! y ∃ x y = A → Ⅎ x y = A
14 2 13 alrimi ⊢ ∃! y ∃ x y = A → ∀ y Ⅎ x y = A
15 dfnfc2 ⊢ ∀ x A ∈ V → Ⅎ _ x A ↔ ∀ y Ⅎ x y = A
16 15 1 mpg ⊢ Ⅎ _ x A ↔ ∀ y Ⅎ x y = A
17 14 16 sylibr ⊢ ∃! y ∃ x y = A → Ⅎ _ x A
18 eusvnfb ⊢ ∃! y ∀ x y = A ↔ Ⅎ _ x A ∧ A ∈ V
19 1 18 mpbiran2 ⊢ ∃! y ∀ x y = A ↔ Ⅎ _ x A
20 eusv2i ⊢ ∃! y ∀ x y = A → ∃! y ∃ x y = A
21 19 20 sylbir ⊢ Ⅎ _ x A → ∃! y ∃ x y = A
22 17 21 impbii ⊢ ∃! y ∃ x y = A ↔ Ⅎ _ x A