Theorem omsson 7716

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 7713	. 2 ⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
2	1	ssrab3 4015	1 ⊢ ω ⊆ On

Syntax hints:   → wi 4  ∀wal 1537   ⊆ wss 3887  Oncon0 6266  Lim wlim 6267  ωcom 7712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-om 7713

This theorem is referenced by:  limomss  7717  nnon  7718  ordom  7722  omssnlim  7727  omsinds  7733  omsindsOLD  7734  nnunifi  9065  unblem1  9066  unblem2  9067  unblem3  9068  unblem4  9069  isfinite2  9072  card2inf  9314  ackbij1lem16  9991  ackbij1lem18  9993  fin23lem26  10081  fin23lem27  10084  isf32lem5  10113  fin1a2lem6  10161  pwfseqlem3  10416  tskinf  10525  grothomex  10585  ltsopi  10644  dmaddpi  10646  dmmulpi  10647  2ndcdisj  22607  finminlem  34507