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 4035	1 ⊢ ω ⊆ On

Syntax hints:   → wi 4  ∀wal 1557   ⊆ wss 3904  Oncon0 6342  Lim wlim 6343  ωcom 7842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3921  df-om 7843

This theorem is referenced by:  limomss  7847  nnon  7848  ordom  7852  omssnlim  7857  omsinds  7863  nnunifi  9231  unblem1  9232  unblem2  9233  unblem3  9234  unblem4  9235  isfinite2  9238  card2inf  9500  ackbij1lem16  10187  ackbij1lem18  10189  fin23lem26  10279  fin23lem27  10282  isf32lem5  10311  fin1a2lem6  10359  pwfseqlem3  10615  tskinf  10724  grothomex  10784  ltsopi  10843  dmaddpi  10845  dmmulpi  10846  2ndcdisj  23496  finminlem  36642  ttcid  36816  dfttc2g  36830  cantnftermord  43861  omabs2  43873