Theorem ordtr 4414

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

Syntax hints:   → wi 4  ∀wral 2475  Tr wtr 4132  Ord word 4398

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 4402

This theorem is referenced by:  ordelss  4415  ordin  4421  ordtr1  4424  orduniss  4461  ontrci  4463  ordon  4523  ordsucim  4537  ordsucss  4541  onsucsssucr  4546  onintonm  4554  ordsucunielexmid  4568  ordn2lp  4582  onsucuni2  4601  nlimsucg  4603  ordpwsucss  4604  tfrexlem  6401  nnsucuniel  6562  ctmlemr  7183  nnnninf  7201  nnnninfeq  7203  nnnninfeq2  7204  ctinf  12672  nnsf  15736  peano4nninf  15737