Theorem ordwe 6362

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

Syntax hints:   → wi 4  Tr wtr 5226   E cep 5549   We wwe 5602  Ord word 6348

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 6352

This theorem is referenced by:  ordfr  6364  trssord  6366  tz7.5  6370  ordelord  6371  tz7.7  6375  oieu  9545  oiid  9547  hartogslem1  9548  oemapso  9688  cantnf  9699  oemapwe  9700  dfac8b  10037  fin23lem27  10334  om2uzoi  13962  ltweuz  13968  om2noseqoi  28212  wepwso  42992  onfrALTlem3  44495  onfrALTlem3VD  44838