Axiom ax-bj-sn 37056

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 2110	. . . . 5 wff 𝑧 ∈ 𝑦
4		vx	. . . . . 6 setvar 𝑥
5	1, 4	weq 1962	. . . . 5 wff 𝑧 = 𝑥
6	3, 5	wb 206	. . . 4 wff (𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)
7	6, 1	wal 1538	. . 3 wff ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)
8	7, 2	wex 1779	. 2 wff ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)
9	8, 4	wal 1538	1 wff ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)

This axiom is referenced by:  bj-snexg  37057