Theorem omsson 7846

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

Syntax hints:   → wi 4  ∀wal 1538   ⊆ wss 3914  Oncon0 6332  Lim wlim 6333  ωcom 7842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-ss 3931  df-om 7843

This theorem is referenced by:  limomss  7847  nnon  7848  ordom  7852  omssnlim  7857  omsinds  7863  nnunifi  9238  unblem1  9239  unblem2  9240  unblem3  9241  unblem4  9242  isfinite2  9245  card2inf  9508  ackbij1lem16  10187  ackbij1lem18  10189  fin23lem26  10278  fin23lem27  10281  isf32lem5  10310  fin1a2lem6  10358  pwfseqlem3  10613  tskinf  10722  grothomex  10782  ltsopi  10841  dmaddpi  10843  dmmulpi  10844  2ndcdisj  23343  finminlem  36306  cantnftermord  43309  omabs2  43321