Axiom ax-bj-sn

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

	Ref	Expression
Assertion	ax-bj-sn	$$⊢\forall x\exists y\forall z\left(z\in y\leftrightarrow z=x\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		vy	$$setvary$$
2		vz	$$setvarz$$
3	2	cv	$$setvarz$$
4	1	cv	$$setvary$$
5	3 4	wcel	$$wffz\in y$$
6	0	cv	$$setvarx$$
7	3 6	wceq	$$wffz=x$$
8	5 7	wb	$$wff\left(z\in y\leftrightarrow z=x\right)$$
9	8 2	wal	$$wff\forall z\left(z\in y\leftrightarrow z=x\right)$$
10	9 1	wex	$$wff\exists y\forall z\left(z\in y\leftrightarrow z=x\right)$$
11	10 0	wal	$$wff\forall x\exists y\forall z\left(z\in y\leftrightarrow z=x\right)$$