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

Theorem ordelss 6194
 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 6192 . 2 (Ord 𝐴 → Tr 𝐴)
2 trss 5167 . . 3 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
32imp 410 . 2 ((Tr 𝐴𝐵𝐴) → 𝐵𝐴)
41, 3sylan 583 1 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2115   ⊆ wss 3919  Tr wtr 5158  Ord word 6177 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-11 2162  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ral 3138  df-v 3482  df-in 3926  df-ss 3936  df-uni 4825  df-tr 5159  df-ord 6181 This theorem is referenced by:  onfr  6217  onelss  6220  ordtri2or2  6274  onfununi  7974  smores3  7986  tfrlem1  8008  tfrlem9a  8018  tz7.44-2  8039  tz7.44-3  8040  oaabslem  8266  oaabs2  8268  omabslem  8269  omabs  8270  findcard3  8758  nnsdomg  8774  ordiso2  8976  ordtypelem2  8980  ordtypelem6  8984  ordtypelem7  8985  cantnf  9153  cnfcomlem  9159  cardmin2  9425  infxpenlem  9437  iunfictbso  9538  dfac12lem2  9568  dfac12lem3  9569  unctb  9625  ackbij2lem1  9639  ackbij1lem3  9642  ackbij1lem18  9657  ackbij2  9663  ttukeylem6  9934  ttukeylem7  9935  alephexp1  9999  fpwwe2lem8  10057  pwfseqlem3  10080  pwdjundom  10087  fz1isolem  13824  onsuct0  33846  finxpreclem4  34756  grur1cld  40860
 Copyright terms: Public domain W3C validator