Theorem ordtr 4390

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

Assertion

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

Proof of Theorem ordtr

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dford3 4379	. 2 |- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
2	1	simplbi 274	1 |- ( Ord A -> Tr A )

Syntax hints:   -> wi 4   A.wral 2465   Tr wtr 4113   Ord word 4374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-iord 4378

This theorem is referenced by:  ordelss  4391  ordin  4397  ordtr1  4400  orduniss  4437  ontrci  4439  ordon  4497  ordsucim  4511  ordsucss  4515  onsucsssucr  4520  onintonm  4528  ordsucunielexmid  4542  ordn2lp  4556  onsucuni2  4575  nlimsucg  4577  ordpwsucss  4578  tfrexlem  6349  nnsucuniel  6510  ctmlemr  7121  nnnninf  7138  nnnninfeq  7140  nnnninfeq2  7141  ctinf  12445  nnsf  15108  peano4nninf  15109