This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

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