Theorem ordtr 4473

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 4462	. 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 4185   Ord word 4457

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 4461

This theorem is referenced by:  ordelss  4474  ordin  4480  ordtr1  4483  orduniss  4520  ontrci  4522  ordon  4582  ordsucim  4596  ordsucss  4600  onsucsssucr  4605  onintonm  4613  ordsucunielexmid  4627  ordn2lp  4641  onsucuni2  4660  nlimsucg  4662  ordpwsucss  4663  tfrexlem  6495  nnsucuniel  6658  ctmlemr  7298  nnnninf  7316  nnnninfeq  7318  nnnninfeq2  7319  ctinf  13041  nnsf  16543  peano4nninf  16544  nnnninfex  16560