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

Theorem ordelss 4600
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 4598 . 2  |-  ( Ord 
A  ->  Tr  A
)
2 trss 4314 . . 3  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
32imp 420 . 2  |-  ( ( Tr  A  /\  B  e.  A )  ->  B  C_  A )
41, 3sylan 459 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726    C_ wss 3322   Tr wtr 4305   Ord word 4583
This theorem is referenced by:  onfr  4623  onelss  4626  ordtri2or2  4681  onfununi  6606  smores3  6618  tfrlem9a  6650  tz7.44-2  6668  tz7.44-3  6669  oaabslem  6889  oaabs2  6891  omabslem  6892  omabs  6893  findcard3  7353  nnsdomg  7369  ordiso2  7487  ordtypelem2  7491  ordtypelem6  7495  ordtypelem7  7496  cantnf  7652  cnfcomlem  7659  cardmin2  7890  infxpenlem  7900  iunfictbso  8000  dfac12lem2  8029  dfac12lem3  8030  unctb  8090  ackbij2lem1  8104  ackbij1lem3  8107  ackbij1lem18  8122  ackbij2  8128  ttukeylem6  8399  ttukeylem7  8400  alephexp1  8459  fpwwe2lem8  8517  pwfseqlem3  8540  pwcdandom  8547  fz1isolem  11715  onsuct0  26196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-v 2960  df-in 3329  df-ss 3336  df-uni 4018  df-tr 4306  df-ord 4587
  Copyright terms: Public domain W3C validator