Theorem ordtr 4525

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

This proof depends on syntax axioms:   → wi 4  ∀wral 2528  Tr wtr 4231  Ord word 4509

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-iord 4513

This theorem is used by:  ordelss  4526  ordin  4532  ordtr1  4535  orduniss  4572  ontrci  4574  ordon  4635  ordsucim  4649  ordsucss  4653  onsucsssucr  4658  onintonm  4666  ordsucunielexmid  4680  ordn2lp  4694  onsucuni2  4713  nlimsucg  4715  ordpwsucss  4716  tfrexlem  6609  nnsucuniel  6772  ctmlemr  7454  nnnninf  7472  nnnninfeq  7474  nnnninfeq2  7475  ctinf  13379  nnsf  17254  peano4nninf  17255  nnnninfex  17271