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

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

Proof of Theorem ordelss
StepHypRef Expression
1 ordtr 6398 . 2 (Ord 𝐴 → Tr 𝐴)
2 trss 5270 . . 3 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
32imp 406 . 2 ((Tr 𝐴𝐵𝐴) → 𝐵𝐴)
41, 3sylan 580 1 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  wss 3951  Tr wtr 5259  Ord word 6383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-ss 3968  df-uni 4908  df-tr 5260  df-ord 6387
This theorem is referenced by:  onfr  6423  onelss  6426  ordtri2or2  6483  onfununi  8381  smores3  8393  tfrlem1  8416  tfrlem9a  8426  tz7.44-2  8447  tz7.44-3  8448  oaabslem  8685  oaabs2  8687  omabslem  8688  omabs  8689  findcard3  9318  findcard3OLD  9319  nnsdomg  9335  nnsdomgOLD  9336  ordiso2  9555  ordtypelem2  9559  ordtypelem6  9563  ordtypelem7  9564  cantnf  9733  cnfcomlem  9739  ttrcltr  9756  cardmin2  10039  infxpenlem  10053  iunfictbso  10154  dfac12lem2  10185  dfac12lem3  10186  unctb  10244  ackbij2lem1  10258  ackbij1lem3  10261  ackbij1lem18  10276  ackbij2  10282  ttukeylem6  10554  ttukeylem7  10555  alephexp1  10619  fpwwe2lem7  10677  pwfseqlem3  10700  pwdjundom  10707  fz1isolem  14500  noinfbday  27765  onsuct0  36442  finxpreclem4  37395  nadd2rabtr  43397  grur1cld  44251
  Copyright terms: Public domain W3C validator