Theorem ordtr 4380

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 4369	. 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 2455   Tr wtr 4103   Ord word 4364

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 4368

This theorem is referenced by:  ordelss  4381  ordin  4387  ordtr1  4390  orduniss  4427  ontrci  4429  ordon  4487  ordsucim  4501  ordsucss  4505  onsucsssucr  4510  onintonm  4518  ordsucunielexmid  4532  ordn2lp  4546  onsucuni2  4565  nlimsucg  4567  ordpwsucss  4568  tfrexlem  6337  nnsucuniel  6498  ctmlemr  7109  nnnninf  7126  nnnninfeq  7128  nnnninfeq2  7129  ctinf  12433  nnsf  14839  peano4nninf  14840