Theorem ordtr 4468

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

Syntax hints:   → wi 4  ∀wral 2508  Tr wtr 4181  Ord word 4452

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

This theorem depends on definitions:  df-bi 117  df-iord 4456

This theorem is referenced by:  ordelss  4469  ordin  4475  ordtr1  4478  orduniss  4515  ontrci  4517  ordon  4577  ordsucim  4591  ordsucss  4595  onsucsssucr  4600  onintonm  4608  ordsucunielexmid  4622  ordn2lp  4636  onsucuni2  4655  nlimsucg  4657  ordpwsucss  4658  tfrexlem  6478  nnsucuniel  6639  ctmlemr  7271  nnnninf  7289  nnnninfeq  7291  nnnninfeq2  7292  ctinf  12996  nnsf  16330  peano4nninf  16331  nnnninfex  16347