Theorem ordtr 4426

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

Syntax hints:   → wi 4  ∀wral 2484  Tr wtr 4143  Ord word 4410

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 4414

This theorem is referenced by:  ordelss  4427  ordin  4433  ordtr1  4436  orduniss  4473  ontrci  4475  ordon  4535  ordsucim  4549  ordsucss  4553  onsucsssucr  4558  onintonm  4566  ordsucunielexmid  4580  ordn2lp  4594  onsucuni2  4613  nlimsucg  4615  ordpwsucss  4616  tfrexlem  6422  nnsucuniel  6583  ctmlemr  7212  nnnninf  7230  nnnninfeq  7232  nnnninfeq2  7233  ctinf  12834  nnsf  15979  peano4nninf  15980  nnnninfex  15996