Theorem ordtr 4300

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

Syntax hints:   → wi 4  ∀wral 2416  Tr wtr 4026  Ord word 4284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-iord 4288

This theorem is referenced by:  ordelss  4301  ordin  4307  ordtr1  4310  orduniss  4347  ontrci  4349  ordon  4402  ordsucim  4416  ordsucss  4420  onsucsssucr  4425  onintonm  4433  ordsucunielexmid  4446  ordn2lp  4460  onsucuni2  4479  nlimsucg  4481  ordpwsucss  4482  tfrexlem  6231  nnsucuniel  6391  ctmlemr  6993  nnnninf  7023  ctinf  11943  nnsf  13199  peano4nninf  13200  nninfalllemn  13202