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	|- ( CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wac	|- CHOICE
1		vx	|- x
2		vf	|- f
3	2	cv	|- f
4	1	cv	|- x
5	3 4	wss	|- f C_ x
6	4	cdm	|- dom x
7	3 6	wfn	|- f Fn dom x
8	5 7	wa	|- ( f C_ x /\ f Fn dom x )
9	8 2	wex	|- E. f ( f C_ x /\ f Fn dom x )
10	9 1	wal	|- A. x E. f ( f C_ x /\ f Fn dom x )
11	0 10	wb	|- ( CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )