Theorem ordtr 4481

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

Syntax hints:   → wi 4  ∀wral 2511  Tr wtr 4192  Ord word 4465

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 4469

This theorem is referenced by:  ordelss  4482  ordin  4488  ordtr1  4491  orduniss  4528  ontrci  4530  ordon  4590  ordsucim  4604  ordsucss  4608  onsucsssucr  4613  onintonm  4621  ordsucunielexmid  4635  ordn2lp  4649  onsucuni2  4668  nlimsucg  4670  ordpwsucss  4671  tfrexlem  6543  nnsucuniel  6706  ctmlemr  7367  nnnninf  7385  nnnninfeq  7387  nnnninfeq2  7388  ctinf  13131  nnsf  16731  peano4nninf  16732  nnnninfex  16748