Theorem bj-snexg

Description: A singleton built on a set is a set. Contrary to bj-snex , this proof is intuitionistically valid and does not require ax-nul . (Contributed by NM, 7-Aug-1994) Extract it from snex and prove it from ax-bj-sn . (Revised by BJ, 12-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-snexg	|- ( A e. V -> { A } e. _V )

Proof

Step	Hyp	Ref	Expression
1		sneq	|- ( x = A -> { x } = { A } )
2		ax-bj-sn	|- A. x E. y A. z ( z e. y <-> z = x )
3	2	spi	|- E. y A. z ( z e. y <-> z = x )
4		bj-axsn	|- ( { x } e. _V <-> E. y A. z ( z e. y <-> z = x ) )
5	3 4	mpbir	|- { x } e. _V
6	1 5	eqeltrrdi	|- ( x = A -> { A } e. _V )
7	6	vtocleg	|- ( A e. V -> { A } e. _V )