Theorem ordtr 4115

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

Syntax hints:   → wi 4  ∀wral 2306  Tr wtr 3854  Ord word 4099

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

This theorem depends on definitions:  df-bi 110  df-iord 4103

This theorem is referenced by:  ordelss  4116  ordin  4122  ordtr1  4125  orduniss  4162  ontrci  4164  ordon  4212  ordsucim  4226  ordsucss  4230  onsucsssucr  4235  onintonm  4243  ordsucunielexmid  4256  ordn2lp  4269  onsucuni2  4288  nlimsucg  4290  ordpwsucss  4291  tfrexlem  5948