Theorem omsson 7892

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

Syntax hints:   → wi 4  ∀wal 1537   ⊆ wss 3950  Oncon0 6383  Lim wlim 6384  ωcom 7888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-ss 3967  df-om 7889

This theorem is referenced by:  limomss  7893  nnon  7894  ordom  7898  omssnlim  7903  omsinds  7909  nnunifi  9328  unblem1  9329  unblem2  9330  unblem3  9331  unblem4  9332  isfinite2  9335  card2inf  9596  ackbij1lem16  10275  ackbij1lem18  10277  fin23lem26  10366  fin23lem27  10369  isf32lem5  10398  fin1a2lem6  10446  pwfseqlem3  10701  tskinf  10810  grothomex  10870  ltsopi  10929  dmaddpi  10931  dmmulpi  10932  2ndcdisj  23465  finminlem  36320  cantnftermord  43338  omabs2  43350