Theorem ordwe 6376

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

Syntax hints:   → wi 4  Tr wtr 5239   E cep 5563   We wwe 5616  Ord word 6362

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 6366

This theorem is referenced by:  ordfr  6378  trssord  6380  tz7.5  6384  ordelord  6385  tz7.7  6389  oieu  9561  oiid  9563  hartogslem1  9564  oemapso  9704  cantnf  9715  oemapwe  9716  dfac8b  10053  fin23lem27  10350  om2uzoi  13978  ltweuz  13984  om2noseqoi  28245  wepwso  43018  onfrALTlem3  44521  onfrALTlem3VD  44864