Theorem omsson 7817

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

Syntax hints:   → wi 4  ∀wal 1545   ⊆ wss 3890  Oncon0 6317  Lim wlim 6318  ωcom 7813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-ss 3907  df-om 7814

This theorem is referenced by:  limomss  7818  nnon  7819  ordom  7823  omssnlim  7828  omsinds  7834  nnunifi  9198  unblem1  9199  unblem2  9200  unblem3  9201  unblem4  9202  isfinite2  9205  card2inf  9467  ackbij1lem16  10154  ackbij1lem18  10156  fin23lem26  10245  fin23lem27  10248  isf32lem5  10277  fin1a2lem6  10325  pwfseqlem3  10581  tskinf  10690  grothomex  10750  ltsopi  10809  dmaddpi  10811  dmmulpi  10812  2ndcdisj  23446  finminlem  36553  ttcid  36727  dfttc2g  36741  cantnftermord  43772  omabs2  43784