Theorem ordtr 4379

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

Syntax hints:   → wi 4  ∀wral 2455  Tr wtr 4102  Ord word 4363

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 4367

This theorem is referenced by:  ordelss  4380  ordin  4386  ordtr1  4389  orduniss  4426  ontrci  4428  ordon  4486  ordsucim  4500  ordsucss  4504  onsucsssucr  4509  onintonm  4517  ordsucunielexmid  4531  ordn2lp  4545  onsucuni2  4564  nlimsucg  4566  ordpwsucss  4567  tfrexlem  6335  nnsucuniel  6496  ctmlemr  7107  nnnninf  7124  nnnninfeq  7126  nnnninfeq2  7127  ctinf  12431  nnsf  14757  peano4nninf  14758