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\in V\to \exists xx\mathrm{We}A$$

Proof

Step	Hyp	Ref	Expression
1		weeq2	$$⊢y=A\to \left(x\mathrm{We}y\leftrightarrow x\mathrm{We}A\right)$$
2	1	exbidv	$$⊢y=A\to \left(\exists xx\mathrm{We}y\leftrightarrow \exists xx\mathrm{We}A\right)$$
3		dfac8	$$⊢\mathrm{CHOICE}\leftrightarrow \forall y\exists xx\mathrm{We}y$$
4	3	axaci	$$⊢\exists xx\mathrm{We}y$$
5	2 4	vtoclg	$$⊢A\in V\to \exists xx\mathrm{We}A$$