Theorem omsson 7859

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

Syntax hints:   → wi 4  ∀wal 1540   ⊆ wss 3949  Oncon0 6365  Lim wlim 6366  ωcom 7855

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-om 7856

This theorem is referenced by:  limomss  7860  nnon  7861  ordom  7865  omssnlim  7870  omsinds  7876  omsindsOLD  7877  nnunifi  9294  unblem1  9295  unblem2  9296  unblem3  9297  unblem4  9298  isfinite2  9301  card2inf  9550  ackbij1lem16  10230  ackbij1lem18  10232  fin23lem26  10320  fin23lem27  10323  isf32lem5  10352  fin1a2lem6  10400  pwfseqlem3  10655  tskinf  10764  grothomex  10824  ltsopi  10883  dmaddpi  10885  dmmulpi  10886  2ndcdisj  22960  finminlem  35251  cantnftermord  42118  omabs2  42130