Theorem onnevOLD

Description: Obsolete version of onnev as of 27-May-2024. (Contributed by NM, 16-Jun-2007) (Proof shortened by Mario Carneiro, 10-Jan-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	onnevOLD	⊢ On ≠ V

Proof

Step	Hyp	Ref	Expression
1		snsn0non	⊢ ¬ { { ∅ } } ∈ On
2		snex	⊢ { { ∅ } } ∈ V
3		id	⊢ ( On = V → On = V )
4	2 3	eleqtrrid	⊢ ( On = V → { { ∅ } } ∈ On )
5	4	necon3bi	⊢ ( ¬ { { ∅ } } ∈ On → On ≠ V )
6	1 5	ax-mp	⊢ On ≠ V