Theorem ordtr 4356

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

Syntax hints:   → wi 4  ∀wral 2444  Tr wtr 4080  Ord word 4340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-iord 4344

This theorem is referenced by:  ordelss  4357  ordin  4363  ordtr1  4366  orduniss  4403  ontrci  4405  ordon  4463  ordsucim  4477  ordsucss  4481  onsucsssucr  4486  onintonm  4494  ordsucunielexmid  4508  ordn2lp  4522  onsucuni2  4541  nlimsucg  4543  ordpwsucss  4544  tfrexlem  6302  nnsucuniel  6463  ctmlemr  7073  nnnninf  7090  nnnninfeq  7092  nnnninfeq2  7093  ctinf  12363  nnsf  13895  peano4nninf  13896