Theorem ordtr 4518

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

Syntax hints:   → wi 4  ∀wral 2528  Tr wtr 4224  Ord word 4502

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 4506

This theorem is referenced by:  ordelss  4519  ordin  4525  ordtr1  4528  orduniss  4565  ontrci  4567  ordon  4628  ordsucim  4642  ordsucss  4646  onsucsssucr  4651  onintonm  4659  ordsucunielexmid  4673  ordn2lp  4687  onsucuni2  4706  nlimsucg  4708  ordpwsucss  4709  tfrexlem  6595  nnsucuniel  6758  ctmlemr  7438  nnnninf  7456  nnnninfeq  7458  nnnninfeq2  7459  ctinf  13299  nnsf  16953  peano4nninf  16954  nnnninfex  16970