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

Theorem ordelss 4899
Description: An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
Assertion
Ref Expression
ordelss

Proof of Theorem ordelss
StepHypRef Expression
1 ordtr 4897 . 2
2 trss 4554 . . 3
32imp 429 . 2
41, 3sylan 471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  C_wss 3475  Trwtr 4545  Ordword 4882
This theorem is referenced by:  onfr  4922  onelss  4925  ordtri2or2  4979  onfununi  7031  smores3  7043  tfrlem1  7064  tfrlem9a  7074  tz7.44-2  7092  tz7.44-3  7093  oaabslem  7311  oaabs2  7313  omabslem  7314  omabs  7315  findcard3  7783  nnsdomg  7799  ordiso2  7961  ordtypelem2  7965  ordtypelem6  7969  ordtypelem7  7970  cantnf  8133  cantnfOLD  8155  cnfcomlem  8164  cnfcomlemOLD  8172  cardmin2  8400  infxpenlem  8412  iunfictbso  8516  dfac12lem2  8545  dfac12lem3  8546  unctb  8606  ackbij2lem1  8620  ackbij1lem3  8623  ackbij1lem18  8638  ackbij2  8644  ttukeylem6  8915  ttukeylem7  8916  alephexp1  8975  fpwwe2lem8  9036  pwfseqlem3  9059  pwcdandom  9066  fz1isolem  12510  onsuct0  29906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111  df-in 3482  df-ss 3489  df-uni 4250  df-tr 4546  df-ord 4886
  Copyright terms: Public domain W3C validator