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

Theorem ordelss 4731
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 4729 . 2  |-  ( Ord 
A  ->  Tr  A
)
2 trss 4391 . . 3  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
32imp 429 . 2  |-  ( ( Tr  A  /\  B  e.  A )  ->  B  C_  A )
41, 3sylan 468 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1761    C_ wss 3325   Tr wtr 4382   Ord word 4714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-v 2972  df-in 3332  df-ss 3339  df-uni 4089  df-tr 4383  df-ord 4718
This theorem is referenced by:  onfr  4754  onelss  4757  ordtri2or2  4811  onfununi  6798  smores3  6810  tfrlem1  6831  tfrlem9a  6841  tz7.44-2  6859  tz7.44-3  6860  oaabslem  7078  oaabs2  7080  omabslem  7081  omabs  7082  findcard3  7551  nnsdomg  7567  ordiso2  7725  ordtypelem2  7729  ordtypelem6  7733  ordtypelem7  7734  cantnf  7897  cantnfOLD  7919  cnfcomlem  7928  cnfcomlemOLD  7936  cardmin2  8164  infxpenlem  8176  iunfictbso  8280  dfac12lem2  8309  dfac12lem3  8310  unctb  8370  ackbij2lem1  8384  ackbij1lem3  8387  ackbij1lem18  8402  ackbij2  8408  ttukeylem6  8679  ttukeylem7  8680  alephexp1  8739  fpwwe2lem8  8800  pwfseqlem3  8823  pwcdandom  8830  fz1isolem  12210  onsuct0  28217
  Copyright terms: Public domain W3C validator