Theorem ordtr 4410

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

Syntax hints:   → wi 4  ∀wral 2472  Tr wtr 4128  Ord word 4394

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 4398

This theorem is referenced by:  ordelss  4411  ordin  4417  ordtr1  4420  orduniss  4457  ontrci  4459  ordon  4519  ordsucim  4533  ordsucss  4537  onsucsssucr  4542  onintonm  4550  ordsucunielexmid  4564  ordn2lp  4578  onsucuni2  4597  nlimsucg  4599  ordpwsucss  4600  tfrexlem  6389  nnsucuniel  6550  ctmlemr  7169  nnnninf  7187  nnnninfeq  7189  nnnninfeq2  7190  ctinf  12590  nnsf  15565  peano4nninf  15566