Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-acn Structured version   Unicode version

Definition df-acn 7860
 Description: Define a local and length-limited version of the axiom of choice. The definition of the predicate AC is that for all families of nonempty subsets of indexed on (i.e. functions ), 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
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-acn
StepHypRef Expression
1 cA . . 3
21wacn 7856 . 2 AC
3 cvv 2962 . . . . 5
41, 3wcel 1727 . . . 4
5 vy . . . . . . . . . 10
65cv 1652 . . . . . . . . 9
7 vg . . . . . . . . . 10
87cv 1652 . . . . . . . . 9
96, 8cfv 5483 . . . . . . . 8
10 vf . . . . . . . . . 10
1110cv 1652 . . . . . . . . 9
126, 11cfv 5483 . . . . . . . 8
139, 12wcel 1727 . . . . . . 7
1413, 5, 1wral 2711 . . . . . 6
1514, 7wex 1551 . . . . 5
16 vx . . . . . . . . 9
1716cv 1652 . . . . . . . 8
1817cpw 3823 . . . . . . 7
19 c0 3613 . . . . . . . 8
2019csn 3838 . . . . . . 7
2118, 20cdif 3303 . . . . . 6
22 cmap 7047 . . . . . 6
2321, 1, 22co 6110 . . . . 5
2415, 10, 23wral 2711 . . . 4
254, 24wa 360 . . 3
2625, 16cab 2428 . 2
272, 26wceq 1653 1 AC
 Colors of variables: wff set class This definition is referenced by:  acnrcl  7954  acneq  7955  isacn  7956
 Copyright terms: Public domain W3C validator