Theorem omsson 7814

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

Syntax hints:   → wi 4  ∀wal 1540   ⊆ wss 3890  Oncon0 6317  Lim wlim 6318  ωcom 7810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-ss 3907  df-om 7811

This theorem is referenced by:  limomss  7815  nnon  7816  ordom  7820  omssnlim  7825  omsinds  7831  nnunifi  9194  unblem1  9195  unblem2  9196  unblem3  9197  unblem4  9198  isfinite2  9201  card2inf  9463  ackbij1lem16  10147  ackbij1lem18  10149  fin23lem26  10238  fin23lem27  10241  isf32lem5  10270  fin1a2lem6  10318  pwfseqlem3  10574  tskinf  10683  grothomex  10743  ltsopi  10802  dmaddpi  10804  dmmulpi  10805  2ndcdisj  23431  finminlem  36516  ttcid  36690  dfttc2g  36704  cantnftermord  43766  omabs2  43778