Theorem omsson 7875

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ⊆ wss 3908  Oncon0 6367  Lim wlim 6368  ωcom 7871

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-ss 3925  df-om 7872

This theorem is used by:  limomss  7876  nnon  7877  ordom  7881  omssnlim  7886  omsinds  7892  nnunifi  9261  unblem1  9262  unblem2  9263  unblem3  9264  unblem4  9265  isfinite2  9268  card2inf  9527  ackbij1lem16  10236  ackbij1lem18  10238  fin23lem26  10327  fin23lem27  10330  isf32lem5  10359  fin1a2lem6  10407  pwfseqlem3  10663  tskinf  10772  grothomex  10832  ltsopi  10891  dmaddpi  10893  dmmulpi  10894  2ndcdisj  23650  finminlem  36869  ttcid  37043  dfttc2g  37057  cantnftermord  44087  omabs2  44099