Definition df-acn 8768

Description: Define a local and length-limited version of the axiom of choice. The definition of the predicate X e. AC A is that for all families of nonempty subsets of X indexed on A (i.e. functions A --> ~P X \ { (/) }), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015.)

Assertion

Ref	Expression
df-acn	|- AC A = { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }

Distinct variable group:   f, g, x, y, A

Detailed syntax breakdown of Definition df-acn

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wacn 8764	. 2 class AC A
3		cvv 3200	. . . . 5 class _V
4	1, 3	wcel 1990	. . . 4 wff A e. _V
5		vy	. . . . . . . . . 10 setvar y
6	5	cv 1482	. . . . . . . . 9 class y
7		vg	. . . . . . . . . 10 setvar g
8	7	cv 1482	. . . . . . . . 9 class g
9	6, 8	cfv 5888	. . . . . . . 8 class ( g ` y )
10		vf	. . . . . . . . . 10 setvar f
11	10	cv 1482	. . . . . . . . 9 class f
12	6, 11	cfv 5888	. . . . . . . 8 class ( f ` y )
13	9, 12	wcel 1990	. . . . . . 7 wff ( g ` y ) e. ( f ` y )
14	13, 5, 1	wral 2912	. . . . . 6 wff A. y e. A ( g ` y ) e. ( f ` y )
15	14, 7	wex 1704	. . . . 5 wff E. g A. y e. A ( g ` y ) e. ( f ` y )
16		vx	. . . . . . . . 9 setvar x
17	16	cv 1482	. . . . . . . 8 class x
18	17	cpw 4158	. . . . . . 7 class ~P x
19		c0 3915	. . . . . . . 8 class (/)
20	19	csn 4177	. . . . . . 7 class { (/) }
21	18, 20	cdif 3571	. . . . . 6 class ( ~P x \ { (/) } )
22		cmap 7857	. . . . . 6 class ^m
23	21, 1, 22	co 6650	. . . . 5 class ( ( ~P x \ { (/) } ) ^m A )
24	15, 10, 23	wral 2912	. . . 4 wff A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y )
25	4, 24	wa 384	. . 3 wff ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) )
26	25, 16	cab 2608	. 2 class { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }
27	2, 26	wceq 1483	1 wff AC A = { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }

This definition is referenced by:  acnrcl  8865  acneq  8866  isacn  8867