Theorem omsson 7881

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ⊆ wss 3895  Oncon0 6362  Lim wlim 6363  ωcom 7877

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896  df-om 7878

This theorem is used by:  limomss  7882  nnon  7883  ordom  7887  omssnlim  7892  omsinds  7898  nnunifi  9286  unblem1  9287  unblem2  9288  unblem3  9289  unblem4  9290  isfinite2  9293  card2inf  9552  ackbij1lem16  10315  ackbij1lem18  10317  fin23lem26  10406  fin23lem27  10409  isf32lem5  10438  fin1a2lem6  10486  pwfseqlem3  10748  tskinf  10857  grothomex  10917  ltsopi  10976  dmaddpi  10978  dmmulpi  10979  2ndcdisj  23780  finminlem  37198  ttcid  37372  dfttc2g  37386  mh-inf3f1  37421  cantnftermord  44415  omabs2  44427