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	$⊢ \{A\} \in V$

Proof

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

Metamath Proof Explorer

Theorem snexALT

Proof