Axiom ax-bj-sn 35704

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

Assertion

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

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Axiom ax-bj-sn

Step	Hyp	Ref	Expression
1		vz	. . . . . 6 setvar 𝑧
2		vy	. . . . . 6 setvar 𝑦
3	1, 2	wel 2107	. . . . 5 wff 𝑧 ∈ 𝑦
4		vx	. . . . . 6 setvar 𝑥
5	1, 4	weq 1966	. . . . 5 wff 𝑧 = 𝑥
6	3, 5	wb 205	. . . 4 wff (𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)
7	6, 1	wal 1539	. . 3 wff ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)
8	7, 2	wex 1781	. 2 wff ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)
9	8, 4	wal 1539	1 wff ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)

This axiom is referenced by:  bj-snexg  35705