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	⊢ ω ⊆ On

Proof

Step	Hyp	Ref	Expression
1		df-om	⊢ ω = { 𝑥 ∈ On ∣ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) }
2	1	ssrab3	⊢ ω ⊆ On