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

Theorem omsson 7811
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 7808 . 2 ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦𝑥𝑦)}
21ssrab3 4045 1 ω ⊆ On
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wss 3915  Oncon0 6322  Lim wlim 6323  ωcom 7807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-in 3922  df-ss 3932  df-om 7808
This theorem is referenced by:  limomss  7812  nnon  7813  ordom  7817  omssnlim  7822  omsinds  7828  omsindsOLD  7829  nnunifi  9245  unblem1  9246  unblem2  9247  unblem3  9248  unblem4  9249  isfinite2  9252  card2inf  9498  ackbij1lem16  10178  ackbij1lem18  10180  fin23lem26  10268  fin23lem27  10271  isf32lem5  10300  fin1a2lem6  10348  pwfseqlem3  10603  tskinf  10712  grothomex  10772  ltsopi  10831  dmaddpi  10833  dmmulpi  10834  2ndcdisj  22823  finminlem  34819  cantnftermord  41684  omabs2  41696
  Copyright terms: Public domain W3C validator