MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  omsson Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 df-om 7889 . 2 ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦𝑥𝑦)}
21ssrab3 4081 1 ω ⊆ On
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator