Axiom ax-bj-sn

Description: Axiom of singleton. (Contributed by BJ, 12-Jan-2025)

	Ref	Expression
Assertion	ax-bj-sn	⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		vy	⊢ 𝑦
2		vz	⊢ 𝑧
3	2	cv	⊢ 𝑧
4	1	cv	⊢ 𝑦
5	3 4	wcel	⊢ 𝑧 ∈ 𝑦
6	0	cv	⊢ 𝑥
7	3 6	wceq	⊢ 𝑧 = 𝑥
8	5 7	wb	⊢ ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 )
9	8 2	wal	⊢ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 )
10	9 1	wex	⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 )
11	10 0	wal	⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 )