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

Theorem ordelss 5893
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 5891 . 2 (Ord 𝐴 → Tr 𝐴)
2 trss 4908 . . 3 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
32imp 394 . 2 ((Tr 𝐴𝐵𝐴) → 𝐵𝐴)
41, 3sylan 570 1 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2148  wss 3729  Tr wtr 4899  Ord word 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ral 3069  df-v 3357  df-in 3736  df-ss 3743  df-uni 4586  df-tr 4900  df-ord 5880
This theorem is referenced by:  onfr  5917  onelss  5920  ordtri2or2  5977  onfununi  7612  smores3  7624  tfrlem1  7646  tfrlem9a  7656  tz7.44-2  7677  tz7.44-3  7678  oaabslem  7898  oaabs2  7900  omabslem  7901  omabs  7902  findcard3  8380  nnsdomg  8396  ordiso2  8597  ordtypelem2  8601  ordtypelem6  8605  ordtypelem7  8606  cantnf  8775  cnfcomlem  8781  cardmin2  9045  infxpenlem  9057  iunfictbso  9158  dfac12lem2  9189  dfac12lem3  9190  unctb  9250  ackbij2lem1  9264  ackbij1lem3  9267  ackbij1lem18  9282  ackbij2  9288  ttukeylem6  9559  ttukeylem7  9560  alephexp1  9624  fpwwe2lem8  9682  pwfseqlem3  9705  pwcdandom  9712  fz1isolem  13469  onsuct0  32794  finxpreclem4  33585
  Copyright terms: Public domain W3C validator