Theorem omsson 7907

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

Syntax hints:   → wi 4  ∀wal 1535   ⊆ wss 3976  Oncon0 6395  Lim wlim 6396  ωcom 7903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-ss 3993  df-om 7904

This theorem is referenced by:  limomss  7908  nnon  7909  ordom  7913  omssnlim  7918  omsinds  7924  omsindsOLD  7925  nnunifi  9355  unblem1  9356  unblem2  9357  unblem3  9358  unblem4  9359  isfinite2  9362  card2inf  9624  ackbij1lem16  10303  ackbij1lem18  10305  fin23lem26  10394  fin23lem27  10397  isf32lem5  10426  fin1a2lem6  10474  pwfseqlem3  10729  tskinf  10838  grothomex  10898  ltsopi  10957  dmaddpi  10959  dmmulpi  10960  2ndcdisj  23485  finminlem  36284  cantnftermord  43282  omabs2  43294