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  6500  nnsucuniel  6663  ctmlemr  7307  nnnninf  7325  nnnninfeq  7327  nnnninfeq2  7328  ctinf  13069  nnsf  16658  peano4nninf  16659  nnnninfex  16675