Theorem ordwe 6204

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

Syntax hints:   → wi 4  Tr wtr 5172   E cep 5464   We wwe 5513  Ord word 6190

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 6194

This theorem is referenced by:  ordfr  6206  trssord  6208  tz7.5  6212  ordelord  6213  tz7.7  6217  oieu  9003  oiid  9005  hartogslem1  9006  oemapso  9145  cantnf  9156  oemapwe  9157  dfac8b  9457  fin23lem27  9750  om2uzoi  13324  ltweuz  13330  wepwso  39663  onfrALTlem3  40898  onfrALTlem3VD  41241