Theorem ordwe 6405

Description: Membership well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
ordwe	⊢ (Ord 𝐴 → E We 𝐴)

Proof of Theorem ordwe

Step	Hyp	Ref	Expression
1		df-ord 6395	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simprbi 496	1 ⊢ (Ord 𝐴 → E We 𝐴)

Syntax hints:   → wi 4  Tr wtr 5268   E cep 5592   We wwe 5644  Ord word 6391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-ord 6395

This theorem is referenced by:  ordfr  6407  trssord  6409  tz7.5  6413  ordelord  6414  tz7.7  6418  oieu  9586  oiid  9588  hartogslem1  9589  oemapso  9729  cantnf  9740  oemapwe  9741  dfac8b  10078  fin23lem27  10375  om2uzoi  14002  ltweuz  14008  om2noseqoi  28335  wepwso  43048  onfrALTlem3  44557  onfrALTlem3VD  44900