Theorem 1n0OLD

Description: Obsolete version of 1n0 as of 10-Jun-2026. (Contributed by NM, 26-Dec-2004) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	1n0OLD	⊢ 1o ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		df1o2	⊢ 1o = { ∅ }
2		0ex	⊢ ∅ ∈ V
3	2	snnz	⊢ { ∅ } ≠ ∅
4	1 3	eqnetri	⊢ 1o ≠ ∅