Theorem ordtr 5737

Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
ordtr	|- ( Ord A -> Tr A )

Proof of Theorem ordtr

Step	Hyp	Ref	Expression
1		df-ord 5726	. 2 |- ( Ord A <-> ( Tr A /\ _E We A ) )
2	1	simplbi 476	1 |- ( Ord A -> Tr A )

Syntax hints:   -> wi 4   Tr wtr 4752   _E cep 5028   We wwe 5072   Ord word 5722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-ord 5726

This theorem is referenced by:  ordelss  5739  ordn2lp  5743  ordelord  5745  tz7.7  5749  ordelssne  5750  ordin  5753  ordtr1  5767  orduniss  5821  ontrci  5833  ordunisuc  7032  onuninsuci  7040  limsuc  7049  ordom  7074  elnn  7075  omsinds  7084  dfrecs3  7469  tz7.44-2  7503  cantnflt  8569  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1  8586  cnfcom  8597  axdc3lem2  9273  inar1  9597  efgmnvl  18127  bnj967  31015  dford5  31608  dford3  37595  limsuc2  37611  ordelordALT  38747  onfrALTlem2  38761  ordelordALTVD  39103  onfrALTlem2VD  39125  iunord  42422