Theorem ordtr 4409

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 4398	. 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 2472   Tr wtr 4127   Ord word 4393

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 4397

This theorem is referenced by:  ordelss  4410  ordin  4416  ordtr1  4419  orduniss  4456  ontrci  4458  ordon  4518  ordsucim  4532  ordsucss  4536  onsucsssucr  4541  onintonm  4549  ordsucunielexmid  4563  ordn2lp  4577  onsucuni2  4596  nlimsucg  4598  ordpwsucss  4599  tfrexlem  6387  nnsucuniel  6548  ctmlemr  7167  nnnninf  7185  nnnninfeq  7187  nnnninfeq2  7188  ctinf  12587  nnsf  15495  peano4nninf  15496