Theorem ordtr 4308

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

Syntax hints:   -> wi 4   A.wral 2417   Tr wtr 4034   Ord word 4292

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

This theorem depends on definitions:  df-bi 116  df-iord 4296

This theorem is referenced by:  ordelss  4309  ordin  4315  ordtr1  4318  orduniss  4355  ontrci  4357  ordon  4410  ordsucim  4424  ordsucss  4428  onsucsssucr  4433  onintonm  4441  ordsucunielexmid  4454  ordn2lp  4468  onsucuni2  4487  nlimsucg  4489  ordpwsucss  4490  tfrexlem  6239  nnsucuniel  6399  ctmlemr  7001  nnnninf  7031  ctinf  11979  nnsf  13374  peano4nninf  13375  nninfalllemn  13377