Theorem dfac10

Description: Axiom of Choice equivalent: the cardinality function measures every set. (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Assertion	dfac10	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{dom}\mathrm{card}=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ween	$$⊢x\in \mathrm{dom}\mathrm{card}\leftrightarrow \exists yy\mathrm{We}x$$
2	1	albii	$$⊢\forall xx\in \mathrm{dom}\mathrm{card}\leftrightarrow \forall x\exists yy\mathrm{We}x$$
3		eqv	$$⊢\mathrm{dom}\mathrm{card}=\mathrm{V}\leftrightarrow \forall xx\in \mathrm{dom}\mathrm{card}$$
4		dfac8	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists yy\mathrm{We}x$$
5	2 3 4	3bitr4ri	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{dom}\mathrm{card}=\mathrm{V}$$