Theorem omsson 7870

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ⊆ wss 3902  Oncon0 6361  Lim wlim 6362  ωcom 7866

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 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-ss 3919  df-om 7867

This theorem is used by:  limomss  7871  nnon  7872  ordom  7876  omssnlim  7881  omsinds  7887  nnunifi  9265  unblem1  9266  unblem2  9267  unblem3  9268  unblem4  9269  isfinite2  9272  card2inf  9531  ackbij1lem16  10240  ackbij1lem18  10242  fin23lem26  10331  fin23lem27  10334  isf32lem5  10363  fin1a2lem6  10411  pwfseqlem3  10673  tskinf  10782  grothomex  10842  ltsopi  10901  dmaddpi  10903  dmmulpi  10904  2ndcdisj  23688  finminlem  36945  ttcid  37119  dfttc2g  37133  cantnftermord  44169  omabs2  44181