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		simpl	|- ( ( CHOICE /\ A e. V ) -> CHOICE )
4		dfac10	|- ( CHOICE <-> dom card = _V )
5	3 4	sylib	|- ( ( CHOICE /\ A e. V ) -> dom card = _V )
6	2 5	eleqtrrid	|- ( ( CHOICE /\ A e. V ) -> x e. dom card )
7		numacn	|- ( A e. V -> ( x e. dom card -> x e. AC_ A ) )
8	1 6 7	sylc	|- ( ( CHOICE /\ A e. V ) -> x e. AC_ A )
9	2	a1i	|- ( ( CHOICE /\ A e. V ) -> x e. _V )
10	8 9	2thd	|- ( ( CHOICE /\ A e. V ) -> ( x e. AC_ A <-> x e. _V ) )
11	10	eqrdv	|- ( ( CHOICE /\ A e. V ) -> AC_ A = _V )