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