Theorem omsson 7809

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

Syntax hints:   → wi 4  ∀wal 1539   ⊆ wss 3899  Oncon0 6314  Lim wlim 6315  ωcom 7805

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-ss 3916  df-om 7806

This theorem is referenced by:  limomss  7810  nnon  7811  ordom  7815  omssnlim  7820  omsinds  7826  nnunifi  9185  unblem1  9186  unblem2  9187  unblem3  9188  unblem4  9189  isfinite2  9192  card2inf  9451  ackbij1lem16  10135  ackbij1lem18  10137  fin23lem26  10226  fin23lem27  10229  isf32lem5  10258  fin1a2lem6  10306  pwfseqlem3  10561  tskinf  10670  grothomex  10730  ltsopi  10789  dmaddpi  10791  dmmulpi  10792  2ndcdisj  23381  finminlem  36373  cantnftermord  43427  omabs2  43439