Theorem ordtr 4469

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 4458	. 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 2508   Tr wtr 4182   Ord word 4453

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 4457

This theorem is referenced by:  ordelss  4470  ordin  4476  ordtr1  4479  orduniss  4516  ontrci  4518  ordon  4578  ordsucim  4592  ordsucss  4596  onsucsssucr  4601  onintonm  4609  ordsucunielexmid  4623  ordn2lp  4637  onsucuni2  4656  nlimsucg  4658  ordpwsucss  4659  tfrexlem  6480  nnsucuniel  6641  ctmlemr  7275  nnnninf  7293  nnnninfeq  7295  nnnninfeq2  7296  ctinf  13001  nnsf  16371  peano4nninf  16372  nnnninfex  16388