Description: This theorem asserts that the constant CHOICE is a theorem, thus eliminating it as a hypothesis while assuming ax-ac2 as an axiom. (Contributed by Mario Carneiro, 6-May-2015) (Revised by NM, 20-Dec-2016) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | axac3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ac2 | |
|
2 | 1 | ax-gen | |
3 | dfackm | |
|
4 | 2 3 | mpbir | |