Theorem omsson 7810

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

Syntax hints:   → wi 4  ∀wal 1538   ⊆ wss 3905  Oncon0 6311  Lim wlim 6312  ωcom 7806

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 3397  df-ss 3922  df-om 7807

This theorem is referenced by:  limomss  7811  nnon  7812  ordom  7816  omssnlim  7821  omsinds  7827  nnunifi  9196  unblem1  9197  unblem2  9198  unblem3  9199  unblem4  9200  isfinite2  9203  card2inf  9466  ackbij1lem16  10147  ackbij1lem18  10149  fin23lem26  10238  fin23lem27  10241  isf32lem5  10270  fin1a2lem6  10318  pwfseqlem3  10573  tskinf  10682  grothomex  10742  ltsopi  10801  dmaddpi  10803  dmmulpi  10804  2ndcdisj  23359  finminlem  36291  cantnftermord  43293  omabs2  43305