Metamath Proof Explorer


Theorem weth

Description: Well-ordering theorem: any set A can be well-ordered. This is an equivalent of the Axiom of Choice. Theorem 6 of Suppes p. 242. First proved by Ernst Zermelo (the "Z" in ZFC) in 1904. (Contributed by Mario Carneiro, 5-Jan-2013)

Ref Expression
Assertion weth
|- ( A e. V -> E. x x We A )

Proof

Step Hyp Ref Expression
1 weeq2
 |-  ( y = A -> ( x We y <-> x We A ) )
2 1 exbidv
 |-  ( y = A -> ( E. x x We y <-> E. x x We A ) )
3 dfac8
 |-  ( CHOICE <-> A. y E. x x We y )
4 3 axaci
 |-  E. x x We y
5 2 4 vtoclg
 |-  ( A e. V -> E. x x We A )