MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  onss Structured version   Unicode version

Theorem onss 6405
Description: An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
onss  |-  ( A  e.  On  ->  A  C_  On )

Proof of Theorem onss
StepHypRef Expression
1 eloni 4732 . 2  |-  ( A  e.  On  ->  Ord  A )
2 ordsson 6404 . 2  |-  ( Ord 
A  ->  A  C_  On )
31, 2syl 16 1  |-  ( A  e.  On  ->  A  C_  On )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3331   Ord word 4721   Oncon0 4722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pr 4534  ax-un 6375
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-pss 3347  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-tp 3885  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-tr 4389  df-eprel 4635  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726
This theorem is referenced by:  onuni  6407  onminex  6421  suceloni  6427  onssi  6451  tfi  6467  tfr3  6861  tz7.49  6903  tz7.49c  6904  oacomf1olem  7006  oeeulem  7043  ordtypelem2  7736  cantnfcl  7878  cantnflt  7883  cantnfp1lem3  7891  oemapvali  7895  cantnflem1c  7898  cantnflem1d  7899  cantnflem1  7900  cantnf  7904  cantnfclOLD  7908  cantnfltOLD  7913  cantnfp1lem3OLD  7917  cantnflem1cOLD  7921  cantnflem1dOLD  7922  cantnflem1OLD  7923  cantnfOLD  7926  cnfcom  7936  cnfcom3lem  7939  cnfcomOLD  7944  cnfcom3lemOLD  7947  infxpenlem  8183  ac10ct  8207  dfac12lem1  8315  dfac12lem2  8316  cfeq0  8428  cfsuc  8429  cff1  8430  cfflb  8431  cofsmo  8441  cfsmolem  8442  alephsing  8448  zorn2lem2  8669  ttukeylem3  8683  ttukeylem5  8685  ttukeylem6  8686  inar1  8945  predon  27657  soseq  27718  nobnddown  27845  nofulllem5  27850  ontgval  28280  aomclem6  29415
  Copyright terms: Public domain W3C validator