Theorem ordtr 4425

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

Syntax hints:   → wi 4  ∀wral 2484  Tr wtr 4142  Ord word 4409

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 4413

This theorem is referenced by:  ordelss  4426  ordin  4432  ordtr1  4435  orduniss  4472  ontrci  4474  ordon  4534  ordsucim  4548  ordsucss  4552  onsucsssucr  4557  onintonm  4565  ordsucunielexmid  4579  ordn2lp  4593  onsucuni2  4612  nlimsucg  4614  ordpwsucss  4615  tfrexlem  6420  nnsucuniel  6581  ctmlemr  7210  nnnninf  7228  nnnninfeq  7230  nnnninfeq2  7231  ctinf  12801  nnsf  15942  peano4nninf  15943  nnnninfex  15959