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	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists f\left(f\subseteq x\wedge fFn\mathrm{dom}x\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wac	$$wff\mathrm{CHOICE}$$
1		vx	$$setvarx$$
2		vf	$$setvarf$$
3	2	cv	$$setvarf$$
4	1	cv	$$setvarx$$
5	3 4	wss	$$wfff\subseteq x$$
6	4	cdm	$$class\mathrm{dom}x$$
7	3 6	wfn	$$wfffFn\mathrm{dom}x$$
8	5 7	wa	$$wff\left(f\subseteq x\wedge fFn\mathrm{dom}x\right)$$
9	8 2	wex	$$wff\exists f\left(f\subseteq x\wedge fFn\mathrm{dom}x\right)$$
10	9 1	wal	$$wff\forall x\exists f\left(f\subseteq x\wedge fFn\mathrm{dom}x\right)$$
11	0 10	wb	$$wff\left(\mathrm{CHOICE}\leftrightarrow \forall x\exists f\left(f\subseteq x\wedge fFn\mathrm{dom}x\right)\right)$$