Theorem ordwe 6344

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 6334	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simprbi 500	1 ⊢ (Ord 𝐴 → E We 𝐴)

Syntax hints:   → wi 4  Tr wtr 5197   E cep 5535   We wwe 5588  Ord word 6330

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 209  df-an 399  df-ord 6334

This theorem is referenced by:  ordfr  6346  trssord  6348  tz7.5  6352  ordelord  6353  tz7.7  6357  oieu  9473  oiid  9475  hartogslem1  9476  oemapso  9623  cantnf  9634  oemapwe  9635  dfac8b  9973  fin23lem27  10271  om2uzoi  13954  ltweuz  13960  om2noseqoi  28362  wepwso  43558  onfrALTlem3  45058  onfrALTlem3VD  45400