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 ⊢ Ⅎ 𝑥 𝜑
Assertion axextmo ∃* 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝜑 )

Proof

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