Theorem snexOLD

Description: Obsolete version of snex as of 6-Mar-2026. (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 19-May-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	snexOLD	$$⊢\left\{A\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		snexg	$$⊢A\in \mathrm{V}\to \left\{A\right\}\in \mathrm{V}$$
2		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
3	2	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5	3 4	eqeltrdi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}\in \mathrm{V}$$
6	1 5	pm2.61i	$$⊢\left\{A\right\}\in \mathrm{V}$$