Theorem ordtr 4501

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 4490	. 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 2522   Tr wtr 4210   Ord word 4485

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 4489

This theorem is referenced by:  ordelss  4502  ordin  4508  ordtr1  4511  orduniss  4548  ontrci  4550  ordon  4610  ordsucim  4624  ordsucss  4628  onsucsssucr  4633  onintonm  4641  ordsucunielexmid  4655  ordn2lp  4669  onsucuni2  4688  nlimsucg  4690  ordpwsucss  4691  tfrexlem  6567  nnsucuniel  6730  ctmlemr  7401  nnnninf  7419  nnnninfeq  7421  nnnninfeq2  7422  ctinf  13198  nnsf  16800  peano4nninf  16801  nnnninfex  16817