Theorem ordtr 4133

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

Syntax hints:   → wi 4  ∀wral 2348  Tr wtr 3875  Ord word 4117

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

This theorem depends on definitions:  df-bi 115  df-iord 4121

This theorem is referenced by:  ordelss  4134  ordin  4140  ordtr1  4143  orduniss  4180  ontrci  4182  ordon  4230  ordsucim  4244  ordsucss  4248  onsucsssucr  4253  onintonm  4261  ordsucunielexmid  4274  ordn2lp  4288  onsucuni2  4307  nlimsucg  4309  ordpwsucss  4310  tfrexlem  5971