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

Theorem ordelss 5777
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 5775 . 2 (Ord 𝐴 → Tr 𝐴)
2 trss 4794 . . 3 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
32imp 444 . 2 ((Tr 𝐴𝐵𝐴) → 𝐵𝐴)
41, 3sylan 487 1 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wss 3607  Tr wtr 4785  Ord word 5760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233  df-in 3614  df-ss 3621  df-uni 4469  df-tr 4786  df-ord 5764
This theorem is referenced by:  onfr  5801  onelss  5804  ordtri2or2  5861  onfununi  7483  smores3  7495  tfrlem1  7517  tfrlem9a  7527  tz7.44-2  7548  tz7.44-3  7549  oaabslem  7768  oaabs2  7770  omabslem  7771  omabs  7772  findcard3  8244  nnsdomg  8260  ordiso2  8461  ordtypelem2  8465  ordtypelem6  8469  ordtypelem7  8470  cantnf  8628  cnfcomlem  8634  cardmin2  8862  infxpenlem  8874  iunfictbso  8975  dfac12lem2  9004  dfac12lem3  9005  unctb  9065  ackbij2lem1  9079  ackbij1lem3  9082  ackbij1lem18  9097  ackbij2  9103  ttukeylem6  9374  ttukeylem7  9375  alephexp1  9439  fpwwe2lem8  9497  pwfseqlem3  9520  pwcdandom  9527  fz1isolem  13283  onsuct0  32565  finxpreclem4  33361
  Copyright terms: Public domain W3C validator