Theorem ordelss 4162

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 4161	. 2 |- ( Ord A -> Tr A )
2		trss 3904	. . 3 |- ( Tr A -> ( B e. A -> B C_ A ) )
3	2	imp 122	. 2 |- ( ( Tr A /\ B e. A ) -> B C_ A )
4	1, 3	sylan 277	1 |- ( ( Ord A /\ B e. A ) -> B C_ A )

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1434   C_ wss 2982   Tr wtr 3895   Ord word 4145

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-v 2612  df-in 2988  df-ss 2995  df-uni 3622  df-tr 3896  df-iord 4149

This theorem is referenced by:  ordelord  4164  onelss  4170  ordsuc  4334  smores3  5962  tfrlem1  5977  tfrlemisucaccv  5994  tfrlemiubacc  5999  tfr1onlemsucaccv  6010  tfr1onlemubacc  6015  tfrcllemsucaccv  6023  tfrcllemubacc  6028  nntri1  6160  nnsseleq  6165  fict  6424  infnfi  6451  isinfinf  6453  ordiso2  6540  hashinfuni  9853