Theorem omsson 7800

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

Assertion

Ref	Expression
omsson	⊢ ω ⊆ On

Proof of Theorem omsson

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4  ∀wal 1539   ⊆ wss 3902  Oncon0 6306  Lim wlim 6307  ωcom 7796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3919  df-om 7797

This theorem is referenced by:  limomss  7801  nnon  7802  ordom  7806  omssnlim  7811  omsinds  7817  nnunifi  9175  unblem1  9176  unblem2  9177  unblem3  9178  unblem4  9179  isfinite2  9182  card2inf  9441  ackbij1lem16  10122  ackbij1lem18  10124  fin23lem26  10213  fin23lem27  10216  isf32lem5  10245  fin1a2lem6  10293  pwfseqlem3  10548  tskinf  10657  grothomex  10717  ltsopi  10776  dmaddpi  10778  dmmulpi  10779  2ndcdisj  23369  finminlem  36351  cantnftermord  43352  omabs2  43364