Theorem omsson 7882

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ⊆ wss 3914  Oncon0 6363  Lim wlim 6364  ωcom 7878

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 3915  df-om 7879

This theorem is used by:  limomss  7883  nnon  7884  ordom  7888  omssnlim  7893  omsinds  7899  nnunifi  9284  unblem1  9285  unblem2  9286  unblem3  9287  unblem4  9288  isfinite2  9291  card2inf  9550  ackbij1lem16  10313  ackbij1lem18  10315  fin23lem26  10404  fin23lem27  10407  isf32lem5  10436  fin1a2lem6  10484  pwfseqlem3  10746  tskinf  10855  grothomex  10915  ltsopi  10974  dmaddpi  10976  dmmulpi  10977  2ndcdisj  23776  finminlem  37107  ttcid  37281  dfttc2g  37295  mh-inf3f1  37330  cantnftermord  44323  omabs2  44335