Theorem snexALT

Description: Alternate proof of snex using Power Set ( ax-pow ) instead of Pairing ( ax-pr ). Unlike in the proof of zfpair , Replacement ( ax-rep ) is not needed. (Contributed by NM, 7-Aug-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		snsspw	$$⊢\left\{A\right\}\subseteq 𝒫A$$
2		ssexg	$$⊢\left(\left\{A\right\}\subseteq 𝒫A\wedge 𝒫A\in \mathrm{V}\right)\to \left\{A\right\}\in \mathrm{V}$$
3	1 2	mpan	$$⊢𝒫A\in \mathrm{V}\to \left\{A\right\}\in \mathrm{V}$$
4		pwexg	$$⊢A\in \mathrm{V}\to 𝒫A\in \mathrm{V}$$
5	4	con3i	$$⊢\neg 𝒫A\in \mathrm{V}\to \neg A\in \mathrm{V}$$
6		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
7	6	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
8		0ex	$$⊢\varnothing \in \mathrm{V}$$
9	7 8	eqeltrdi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}\in \mathrm{V}$$
10	5 9	syl	$$⊢\neg 𝒫A\in \mathrm{V}\to \left\{A\right\}\in \mathrm{V}$$
11	3 10	pm2.61i	$$⊢\left\{A\right\}\in \mathrm{V}$$