Definition df-acnm 7258

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 inhabited subsets of X indexed on A (i.e. functions A --> { z e. ~P X | E. j j e. z }), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015.) Change nonempty to inhabited. (Revised by Jim Kingdon, 22-Nov-2025.)

Assertion

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

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

Detailed syntax breakdown of Definition df-acnm

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wacn 7256	. 2 class AC A
3		cvv 2763	. . . . 5 class _V
4	1, 3	wcel 2167	. . . 4 wff A e. _V
5		vy	. . . . . . . . . 10 setvar y
6	5	cv 1363	. . . . . . . . 9 class y
7		vg	. . . . . . . . . 10 setvar g
8	7	cv 1363	. . . . . . . . 9 class g
9	6, 8	cfv 5259	. . . . . . . 8 class ( g ` y )
10		vf	. . . . . . . . . 10 setvar f
11	10	cv 1363	. . . . . . . . 9 class f
12	6, 11	cfv 5259	. . . . . . . 8 class ( f ` y )
13	9, 12	wcel 2167	. . . . . . 7 wff ( g ` y ) e. ( f ` y )
14	13, 5, 1	wral 2475	. . . . . 6 wff A. y e. A ( g ` y ) e. ( f ` y )
15	14, 7	wex 1506	. . . . 5 wff E. g A. y e. A ( g ` y ) e. ( f ` y )
16		vj	. . . . . . . . 9 setvar j
17		vz	. . . . . . . . 9 setvar z
18	16, 17	wel 2168	. . . . . . . 8 wff j e. z
19	18, 16	wex 1506	. . . . . . 7 wff E. j j e. z
20		vx	. . . . . . . . 9 setvar x
21	20	cv 1363	. . . . . . . 8 class x
22	21	cpw 3606	. . . . . . 7 class ~P x
23	19, 17, 22	crab 2479	. . . . . 6 class { z e. ~P x | E. j j e. z }
24		cmap 6716	. . . . . 6 class ^m
25	23, 1, 24	co 5925	. . . . 5 class ( { z e. ~P x | E. j j e. z } ^m A )
26	15, 10, 25	wral 2475	. . . 4 wff A. f e. ( { z e. ~P x | E. j j e. z } ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y )
27	4, 26	wa 104	. . 3 wff ( A e. _V /\ A. f e. ( { z e. ~P x | E. j j e. z } ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) )
28	27, 20	cab 2182	. 2 class { x | ( A e. _V /\ A. f e. ( { z e. ~P x | E. j j e. z } ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }
29	2, 28	wceq 1364	1 wff AC A = { x | ( A e. _V /\ A. f e. ( { z e. ~P x | E. j j e. z } ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }

This definition is referenced by:  acnrcl  7284  acneq  7285  isacnm  7286