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 4030	1 ⊢ ω ⊆ On

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ⊆ wss 3899  Oncon0 6355  Lim wlim 6356  ω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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3916  df-om 7867

This theorem is used by:  limomss  7871  nnon  7872  ordom  7876  omssnlim  7881  omsinds  7887  nnunifi  9267  unblem1  9268  unblem2  9269  unblem3  9270  unblem4  9271  isfinite2  9274  card2inf  9533  ackbij1lem16  10293  ackbij1lem18  10295  fin23lem26  10384  fin23lem27  10387  isf32lem5  10416  fin1a2lem6  10464  pwfseqlem3  10726  tskinf  10835  grothomex  10895  ltsopi  10954  dmaddpi  10956  dmmulpi  10957  2ndcdisj  23755  finminlem  37076  ttcid  37250  dfttc2g  37264  mh-inf3f1  37299  cantnftermord  44280  omabs2  44292