Theorem omsson 7806

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

Syntax hints:   → wi 4  ∀wal 1539   ⊆ wss 3898  Oncon0 6311  Lim wlim 6312  ωcom 7802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-ss 3915  df-om 7803

This theorem is referenced by:  limomss  7807  nnon  7808  ordom  7812  omssnlim  7817  omsinds  7823  nnunifi  9182  unblem1  9183  unblem2  9184  unblem3  9185  unblem4  9186  isfinite2  9189  card2inf  9448  ackbij1lem16  10132  ackbij1lem18  10134  fin23lem26  10223  fin23lem27  10226  isf32lem5  10255  fin1a2lem6  10303  pwfseqlem3  10558  tskinf  10667  grothomex  10727  ltsopi  10786  dmaddpi  10788  dmmulpi  10789  2ndcdisj  23372  finminlem  36383  cantnftermord  43437  omabs2  43449