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

Theorem ordelss 4540
Description: An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
Assertion
Ref Expression
ordelss  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  C_  A )

Proof of Theorem ordelss
StepHypRef Expression
1 ordtr 4538 . 2  |-  ( Ord 
A  ->  Tr  A
)
2 trss 4254 . . 3  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
32imp 419 . 2  |-  ( ( Tr  A  /\  B  e.  A )  ->  B  C_  A )
41, 3sylan 458 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1717    C_ wss 3265   Tr wtr 4245   Ord word 4523
This theorem is referenced by:  onfr  4563  onelss  4566  ordtri2or2  4620  onfununi  6541  smores3  6553  tfrlem9a  6585  tz7.44-2  6603  tz7.44-3  6604  oaabslem  6824  oaabs2  6826  omabslem  6827  omabs  6828  findcard3  7288  nnsdomg  7304  ordiso2  7419  ordtypelem2  7423  ordtypelem6  7427  ordtypelem7  7428  cantnf  7584  cnfcomlem  7591  cardmin2  7820  infxpenlem  7830  iunfictbso  7930  dfac12lem2  7959  dfac12lem3  7960  unctb  8020  ackbij2lem1  8034  ackbij1lem3  8037  ackbij1lem18  8052  ackbij2  8058  ttukeylem6  8329  ttukeylem7  8330  alephexp1  8389  fpwwe2lem8  8447  pwfseqlem3  8470  pwcdandom  8477  fz1isolem  11639  onsuct0  25907
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ral 2656  df-v 2903  df-in 3272  df-ss 3279  df-uni 3960  df-tr 4246  df-ord 4527
  Copyright terms: Public domain W3C validator