Theorem ordelss 5739

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

Step	Hyp	Ref	Expression
1		ordtr 5737	. 2 |- ( Ord A -> Tr A )
2		trss 4761	. . 3 |- ( Tr A -> ( B e. A -> B C_ A ) )
3	2	imp 445	. 2 |- ( ( Tr A /\ B e. A ) -> B C_ A )
4	1, 3	sylan 488	1 |- ( ( Ord A /\ B e. A ) -> B C_ A )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   C_ wss 3574   Tr wtr 4752   Ord word 5722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-in 3581  df-ss 3588  df-uni 4437  df-tr 4753  df-ord 5726

This theorem is referenced by:  onfr  5763  onelss  5766  ordtri2or2  5823  onfununi  7438  smores3  7450  tfrlem1  7472  tfrlem9a  7482  tz7.44-2  7503  tz7.44-3  7504  oaabslem  7723  oaabs2  7725  omabslem  7726  omabs  7727  findcard3  8203  nnsdomg  8219  ordiso2  8420  ordtypelem2  8424  ordtypelem6  8428  ordtypelem7  8429  cantnf  8590  cnfcomlem  8596  cardmin2  8824  infxpenlem  8836  iunfictbso  8937  dfac12lem2  8966  dfac12lem3  8967  unctb  9027  ackbij2lem1  9041  ackbij1lem3  9044  ackbij1lem18  9059  ackbij2  9065  ttukeylem6  9336  ttukeylem7  9337  alephexp1  9401  fpwwe2lem8  9459  pwfseqlem3  9482  pwcdandom  9489  fz1isolem  13245  onsuct0  32440  finxpreclem4  33231