Theorem ordtr 4523

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 4512	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥))
2	1	simplbi 274	1 ⊢ (Ord 𝐴 → Tr 𝐴)

This proof depends on syntax axioms:   → wi 4  ∀wral 2528  Tr wtr 4229  Ord word 4507

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-iord 4511

This theorem is used by:  ordelss  4524  ordin  4530  ordtr1  4533  orduniss  4570  ontrci  4572  ordon  4633  ordsucim  4647  ordsucss  4651  onsucsssucr  4656  onintonm  4664  ordsucunielexmid  4678  ordn2lp  4692  onsucuni2  4711  nlimsucg  4713  ordpwsucss  4714  tfrexlem  6605  nnsucuniel  6768  ctmlemr  7448  nnnninf  7466  nnnninfeq  7468  nnnninfeq2  7469  ctinf  13321  nnsf  17048  peano4nninf  17049  nnnninfex  17065