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		dfac10	⊢ ( CHOICE ↔ dom card = V )
4	3	birani	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → dom card = V )
5	2 4	eleqtrrid	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → 𝑥 ∈ dom card )
6		numacn	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ dom card → 𝑥 ∈ AC 𝐴 ) )
7	1 5 6	sylc	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → 𝑥 ∈ AC 𝐴 )
8	2	a1i	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → 𝑥 ∈ V )
9	7 8	2thd	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ AC 𝐴 ↔ 𝑥 ∈ V ) )
10	9	eqrdv	⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → AC 𝐴 = V )