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 ∧ 𝐴 ∈ 𝑉 ) → AC 𝐴 = V )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
2		vex	⊢ 𝑥 ∈ V
3		simpl	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → CHOICE )
4		dfac10	⊢ ( CHOICE ↔ dom card = V )
5	3 4	sylib	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → dom card = V )
6	2 5	eleqtrrid	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → 𝑥 ∈ dom card )
7		numacn	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ dom card → 𝑥 ∈ AC 𝐴 ) )
8	1 6 7	sylc	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → 𝑥 ∈ AC 𝐴 )
9	2	a1i	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → 𝑥 ∈ V )
10	8 9	2thd	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ AC 𝐴 ↔ 𝑥 ∈ V ) )
11	10	eqrdv	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → AC 𝐴 = V )