Theorem ordtr 4363

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

Syntax hints:   → wi 4  ∀wral 2448  Tr wtr 4087  Ord word 4347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-iord 4351

This theorem is referenced by:  ordelss  4364  ordin  4370  ordtr1  4373  orduniss  4410  ontrci  4412  ordon  4470  ordsucim  4484  ordsucss  4488  onsucsssucr  4493  onintonm  4501  ordsucunielexmid  4515  ordn2lp  4529  onsucuni2  4548  nlimsucg  4550  ordpwsucss  4551  tfrexlem  6313  nnsucuniel  6474  ctmlemr  7085  nnnninf  7102  nnnninfeq  7104  nnnninfeq2  7105  ctinf  12385  nnsf  14038  peano4nninf  14039