Theorem ordtr 4475

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

Syntax hints:   → wi 4  ∀wral 2510  Tr wtr 4187  Ord word 4459

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 4463

This theorem is referenced by:  ordelss  4476  ordin  4482  ordtr1  4485  orduniss  4522  ontrci  4524  ordon  4584  ordsucim  4598  ordsucss  4602  onsucsssucr  4607  onintonm  4615  ordsucunielexmid  4629  ordn2lp  4643  onsucuni2  4662  nlimsucg  4664  ordpwsucss  4665  tfrexlem  6499  nnsucuniel  6662  ctmlemr  7306  nnnninf  7324  nnnninfeq  7326  nnnninfeq2  7327  ctinf  13050  nnsf  16607  peano4nninf  16608  nnnninfex  16624