Theorem ordtr 4203

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 4192	. 2 |- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
2	1	simplbi 268	1 |- ( Ord A -> Tr A )

Syntax hints:   -> wi 4   A.wral 2359   Tr wtr 3934   Ord word 4187

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

This theorem depends on definitions:  df-bi 115  df-iord 4191

This theorem is referenced by:  ordelss  4204  ordin  4210  ordtr1  4213  orduniss  4250  ontrci  4252  ordon  4301  ordsucim  4315  ordsucss  4319  onsucsssucr  4324  onintonm  4332  ordsucunielexmid  4345  ordn2lp  4359  onsucuni2  4378  nlimsucg  4380  ordpwsucss  4381  tfrexlem  6091  nnsucuniel  6248  nnnninf  6796  nnsf  11778  peano4nninf  11779  nninfalllemn  11781