Theorem ordtr 4413

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 4402	. 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 2475   Tr wtr 4131   Ord word 4397

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 4401

This theorem is referenced by:  ordelss  4414  ordin  4420  ordtr1  4423  orduniss  4460  ontrci  4462  ordon  4522  ordsucim  4536  ordsucss  4540  onsucsssucr  4545  onintonm  4553  ordsucunielexmid  4567  ordn2lp  4581  onsucuni2  4600  nlimsucg  4602  ordpwsucss  4603  tfrexlem  6392  nnsucuniel  6553  ctmlemr  7174  nnnninf  7192  nnnninfeq  7194  nnnninfeq2  7195  ctinf  12647  nnsf  15649  peano4nninf  15650