Theorem omsson 7822

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

Syntax hints:   → wi 4  ∀wal 1540   ⊆ wss 3903  Oncon0 6325  Lim wlim 6326  ωcom 7818

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-ss 3920  df-om 7819

This theorem is referenced by:  limomss  7823  nnon  7824  ordom  7828  omssnlim  7833  omsinds  7839  nnunifi  9203  unblem1  9204  unblem2  9205  unblem3  9206  unblem4  9207  isfinite2  9210  card2inf  9472  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  23412  finminlem  36531  cantnftermord  43671  omabs2  43683