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

Metamath Proof Explorer

Theorem axextmo

Description: There exists at most one set with prescribed elements. Theorem 1.1 of BellMachover p. 462. (Contributed by NM, 30-Jun-1994) (Proof shortened by Wolf Lammen, 13-Nov-2019) Use the at-most-one quantifier. (Revised by BJ, 17-Sep-2022)

Ref Expression
Hypothesis axextmo.1 ⊢ Ⅎ x φ
Assertion axextmo ⊢ ∃* x ∀ y y ∈ x ↔ φ

Proof

Step Hyp Ref Expression
1 axextmo.1 ⊢ Ⅎ x φ
2 biantr ⊢ y ∈ x ↔ φ ∧ y ∈ z ↔ φ → y ∈ x ↔ y ∈ z
3 2 alanimi ⊢ ∀ y y ∈ x ↔ φ ∧ ∀ y y ∈ z ↔ φ → ∀ y y ∈ x ↔ y ∈ z
4 ax-ext ⊢ ∀ y y ∈ x ↔ y ∈ z → x = z
5 3 4 syl ⊢ ∀ y y ∈ x ↔ φ ∧ ∀ y y ∈ z ↔ φ → x = z
6 5 gen2 ⊢ ∀ x ∀ z ∀ y y ∈ x ↔ φ ∧ ∀ y y ∈ z ↔ φ → x = z
7 nfv ⊢ Ⅎ x y ∈ z
8 7 1 nfbi ⊢ Ⅎ x y ∈ z ↔ φ
9 8 nfal ⊢ Ⅎ x ∀ y y ∈ z ↔ φ
10 elequ2 ⊢ x = z → y ∈ x ↔ y ∈ z
11 10 bibi1d ⊢ x = z → y ∈ x ↔ φ ↔ y ∈ z ↔ φ
12 11 albidv ⊢ x = z → ∀ y y ∈ x ↔ φ ↔ ∀ y y ∈ z ↔ φ
13 9 12 mo4f ⊢ ∃* x ∀ y y ∈ x ↔ φ ↔ ∀ x ∀ z ∀ y y ∈ x ↔ φ ∧ ∀ y y ∈ z ↔ φ → x = z
14 6 13 mpbir ⊢ ∃* x ∀ y y ∈ x ↔ φ