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	|- ( ( CHOICE /\ A e. V ) -> AC_ A = _V )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( CHOICE /\ A e. V ) -> A e. V )
2		vex	|- x e. _V
3		dfac10	|- ( CHOICE <-> dom card = _V )
4	3	birani	|- ( ( CHOICE /\ A e. V ) -> dom card = _V )
5	2 4	eleqtrrid	|- ( ( CHOICE /\ A e. V ) -> x e. dom card )
6		numacn	|- ( A e. V -> ( x e. dom card -> x e. AC_ A ) )
7	1 5 6	sylc	|- ( ( CHOICE /\ A e. V ) -> x e. AC_ A )
8	2	a1i	|- ( ( CHOICE /\ A e. V ) -> x e. _V )
9	7 8	2thd	|- ( ( CHOICE /\ A e. V ) -> ( x e. AC_ A <-> x e. _V ) )
10	9	eqrdv	|- ( ( CHOICE /\ A e. V ) -> AC_ A = _V )