Metamath Proof Explorer


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 CHOICEAVAC_A=V

Proof

Step Hyp Ref Expression
1 simpr CHOICEAVAV
2 vex xV
3 simpl CHOICEAVCHOICE
4 dfac10 CHOICEdomcard=V
5 3 4 sylib CHOICEAVdomcard=V
6 2 5 eleqtrrid CHOICEAVxdomcard
7 numacn AVxdomcardxAC_A
8 1 6 7 sylc CHOICEAVxAC_A
9 2 a1i CHOICEAVxV
10 8 9 2thd CHOICEAVxAC_AxV
11 10 eqrdv CHOICEAVAC_A=V