Theorem onnev

Description: The class of ordinal numbers is not equal to the universe. (Contributed by NM, 16-Jun-2007) (Proof shortened by Mario Carneiro, 10-Jan-2013)

	Ref	Expression
Assertion	onnev	⊢ 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