Theorem ordtr 4229

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

Syntax hints:   → wi 4  ∀wral 2370  Tr wtr 3958  Ord word 4213

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

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

This theorem is referenced by:  ordelss  4230  ordin  4236  ordtr1  4239  orduniss  4276  ontrci  4278  ordon  4331  ordsucim  4345  ordsucss  4349  onsucsssucr  4354  onintonm  4362  ordsucunielexmid  4375  ordn2lp  4389  onsucuni2  4408  nlimsucg  4410  ordpwsucss  4411  tfrexlem  6137  nnsucuniel  6296  ctmlemr  6870  nnnninf  6894  nnsf  12604  peano4nninf  12605  nninfalllemn  12607