Metamath Proof Explorer

Definition df-acn

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)

Ref Expression
Assertion df-acn ⊢AC_A=x|A∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA classA
1 0 wacn classAC_A
2 vx setvarx
3 cvv classV
4 0 3 wcel wffA∈V
5 vf setvarf
6 2 cv setvarx
7 6 cpw class𝒫x
8 c0 class∅
9 8 csn class∅
10 7 9 cdif class𝒫x∖∅
11 cmap class↑𝑚
12 10 0 11 co class𝒫x∖∅A
13 vg setvarg
14 vy setvary
15 13 cv setvarg
16 14 cv setvary
17 16 15 cfv classg⁡y
18 5 cv setvarf
19 16 18 cfv classf⁡y
20 17 19 wcel wffg⁡y∈f⁡y
21 20 14 0 wral wff∀y∈Ag⁡y∈f⁡y
22 21 13 wex wff∃g∀y∈Ag⁡y∈f⁡y
23 22 5 12 wral wff∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y
24 4 23 wa wffA∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y
25 24 2 cab classx|A∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y
26 1 25 wceq wffAC_A=x|A∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y