Theorem ordtr 4504

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

Syntax hints:   → wi 4  ∀wral 2522  Tr wtr 4213  Ord word 4488

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 4492

This theorem is referenced by:  ordelss  4505  ordin  4511  ordtr1  4514  orduniss  4551  ontrci  4553  ordon  4613  ordsucim  4627  ordsucss  4631  onsucsssucr  4636  onintonm  4644  ordsucunielexmid  4658  ordn2lp  4672  onsucuni2  4691  nlimsucg  4693  ordpwsucss  4694  tfrexlem  6578  nnsucuniel  6741  ctmlemr  7412  nnnninf  7430  nnnninfeq  7432  nnnninfeq2  7433  ctinf  13265  nnsf  16909  peano4nninf  16910  nnnninfex  16926