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 ∈ A g ⁡ y ∈ f ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 wacn class AC _ A
2 vx setvar x
3 cvv class V
4 0 3 wcel wff A ∈ V
5 vf setvar f
6 2 cv setvar x
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 setvar g
14 vy setvar y
15 13 cv setvar g
16 14 cv setvar y
17 16 15 cfv class g ⁡ y
18 5 cv setvar f
19 16 18 cfv class f ⁡ y
20 17 19 wcel wff g ⁡ y ∈ f ⁡ y
21 20 14 0 wral wff ∀ y ∈ A g ⁡ y ∈ f ⁡ y
22 21 13 wex wff ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
23 22 5 12 wral wff ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
24 4 23 wa wff A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
25 24 2 cab class x | A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
26 1 25 wceq wff AC _ A = x | A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y