Axiom ax-bj-sn

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

	Ref	Expression
Assertion	ax-bj-sn	|- A. x E. y A. z ( z e. y <-> z = x )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		vy	|- y
2		vz	|- z
3	2	cv	|- z
4	1	cv	|- y
5	3 4	wcel	|- z e. y
6	0	cv	|- x
7	3 6	wceq	|- z = x
8	5 7	wb	|- ( z e. y <-> z = x )
9	8 2	wal	|- A. z ( z e. y <-> z = x )
10	9 1	wex	|- E. y A. z ( z e. y <-> z = x )
11	10 0	wal	|- A. x E. y A. z ( z e. y <-> z = x )