Metamath Proof Explorer

Theorem ordwe

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

Ref Expression
Assertion ordwe 
|- ( Ord A -> _E We A )

Proof

Step Hyp Ref Expression
1 df-ord 
 |-  ( Ord A <-> ( Tr A /\ _E We A ) )
2 1 simprbi 
 |-  ( Ord A -> _E We A )