Theorem omsson 7821

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

Syntax hints:   → wi 4  ∀wal 1540   ⊆ wss 3889  Oncon0 6323  Lim wlim 6324  ωcom 7817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906  df-om 7818

This theorem is referenced by:  limomss  7822  nnon  7823  ordom  7827  omssnlim  7832  omsinds  7838  nnunifi  9201  unblem1  9202  unblem2  9203  unblem3  9204  unblem4  9205  isfinite2  9208  card2inf  9470  ackbij1lem16  10156  ackbij1lem18  10158  fin23lem26  10247  fin23lem27  10250  isf32lem5  10279  fin1a2lem6  10327  pwfseqlem3  10583  tskinf  10692  grothomex  10752  ltsopi  10811  dmaddpi  10813  dmmulpi  10814  2ndcdisj  23421  finminlem  36500  ttcid  36674  dfttc2g  36688  cantnftermord  43748  omabs2  43760