Theorem ordtr 4372

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

Syntax hints:   → wi 4  ∀wral 2453  Tr wtr 4096  Ord word 4356

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 4360

This theorem is referenced by:  ordelss  4373  ordin  4379  ordtr1  4382  orduniss  4419  ontrci  4421  ordon  4479  ordsucim  4493  ordsucss  4497  onsucsssucr  4502  onintonm  4510  ordsucunielexmid  4524  ordn2lp  4538  onsucuni2  4557  nlimsucg  4559  ordpwsucss  4560  tfrexlem  6325  nnsucuniel  6486  ctmlemr  7097  nnnninf  7114  nnnninfeq  7116  nnnninfeq2  7117  ctinf  12396  nnsf  14295  peano4nninf  14296