Metamath Proof Explorer

Theorem omsson

Description: Omega is a subset of On . (Contributed by NM, 13-Jun-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion omsson 
|- _om C_ On

Proof

Step Hyp Ref Expression
1 df-om 
 |-  _om = { x e. On | A. y ( Lim y -> x e. y ) }
2 1 ssrab3 
 |-  _om C_ On