Theorem ordtr 4469

Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
ordtr	⊢ (Ord 𝐴 → Tr 𝐴)

Proof of Theorem ordtr

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dford3 4458	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥))
2	1	simplbi 274	1 ⊢ (Ord 𝐴 → Tr 𝐴)

Syntax hints:   → wi 4  ∀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  6486  nnsucuniel  6649  ctmlemr  7286  nnnninf  7304  nnnninfeq  7306  nnnninfeq2  7307  ctinf  13017  nnsf  16459  peano4nninf  16460  nnnninfex  16476