Theorem ordtr 4443

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

Syntax hints:   → wi 4  ∀wral 2486  Tr wtr 4158  Ord word 4427

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 4431

This theorem is referenced by:  ordelss  4444  ordin  4450  ordtr1  4453  orduniss  4490  ontrci  4492  ordon  4552  ordsucim  4566  ordsucss  4570  onsucsssucr  4575  onintonm  4583  ordsucunielexmid  4597  ordn2lp  4611  onsucuni2  4630  nlimsucg  4632  ordpwsucss  4633  tfrexlem  6443  nnsucuniel  6604  ctmlemr  7236  nnnninf  7254  nnnninfeq  7256  nnnninfeq2  7257  ctinf  12916  nnsf  16144  peano4nninf  16145  nnnninfex  16161