Theorem acacni

Description: A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	acacni	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to \underset{\_}{\mathrm{AC}}A=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to A\in V$$
2		vex	$$⊢x\in \mathrm{V}$$
3		dfac10	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{dom}\mathrm{card}=\mathrm{V}$$
4	3	birani	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to \mathrm{dom}\mathrm{card}=\mathrm{V}$$
5	2 4	eleqtrrid	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to x\in \mathrm{dom}\mathrm{card}$$
6		numacn	$$⊢A\in V\to \left(x\in \mathrm{dom}\mathrm{card}\to x\in \underset{\_}{\mathrm{AC}}A\right)$$
7	1 5 6	sylc	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to x\in \underset{\_}{\mathrm{AC}}A$$
8	2	a1i	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to x\in \mathrm{V}$$
9	7 8	2thd	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to \left(x\in \underset{\_}{\mathrm{AC}}A\leftrightarrow x\in \mathrm{V}\right)$$
10	9	eqrdv	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to \underset{\_}{\mathrm{AC}}A=\mathrm{V}$$