Metamath Proof Explorer


Definition df-ac

Description: The expression CHOICE will be used as a readable shorthand for any form of the axiom of choice; all concrete forms are long, cryptic, have dummy variables, or all three, making it useful to have a short name. Similar to the Axiom of Choice (first form) of Enderton p. 49.

There is a slight problem with taking the exact form of ax-ac as our definition, because the equivalence to more standard forms ( dfac2 ) requires the Axiom of Regularity, which we often try to avoid. Thus, we take the first of the "textbook forms" as the definition and derive the form of ax-ac itself as dfac0 . (Contributed by Mario Carneiro, 22-Feb-2015)

Ref Expression
Assertion df-ac CHOICExffxfFndomx

Detailed syntax breakdown

Step Hyp Ref Expression
0 wac wffCHOICE
1 vx setvarx
2 vf setvarf
3 2 cv setvarf
4 1 cv setvarx
5 3 4 wss wfffx
6 4 cdm classdomx
7 3 6 wfn wfffFndomx
8 5 7 wa wfffxfFndomx
9 8 2 wex wffffxfFndomx
10 9 1 wal wffxffxfFndomx
11 0 10 wb wffCHOICExffxfFndomx