ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ac GIF version

Definition df-ac 7205
Description: The expression CHOICE will be used as a readable shorthand for any form of the axiom of choice; all concrete forms are long, cryptic, have dummy variables, or all three, making it useful to have a short name. Similar to the Axiom of Choice (first form) of [Enderton] p. 49.

There are some decisions about how to write this definition especially around whether ax-setind 4537 is needed to show equivalence to other ways of stating choice, and about whether choice functions are available for nonempty sets or inhabited sets. (Contributed by Mario Carneiro, 22-Feb-2015.)

Assertion
Ref Expression
df-ac (CHOICE ↔ ∀𝑥𝑓(𝑓𝑥𝑓 Fn dom 𝑥))
Distinct variable group:   𝑥,𝑓

Detailed syntax breakdown of Definition df-ac
StepHypRef Expression
1 wac 7204 . 2 wff CHOICE
2 vf . . . . . . 7 setvar 𝑓
32cv 1352 . . . . . 6 class 𝑓
4 vx . . . . . . 7 setvar 𝑥
54cv 1352 . . . . . 6 class 𝑥
63, 5wss 3130 . . . . 5 wff 𝑓𝑥
75cdm 4627 . . . . . 6 class dom 𝑥
83, 7wfn 5212 . . . . 5 wff 𝑓 Fn dom 𝑥
96, 8wa 104 . . . 4 wff (𝑓𝑥𝑓 Fn dom 𝑥)
109, 2wex 1492 . . 3 wff 𝑓(𝑓𝑥𝑓 Fn dom 𝑥)
1110, 4wal 1351 . 2 wff 𝑥𝑓(𝑓𝑥𝑓 Fn dom 𝑥)
121, 11wb 105 1 wff (CHOICE ↔ ∀𝑥𝑓(𝑓𝑥𝑓 Fn dom 𝑥))
Colors of variables: wff set class
This definition is referenced by:  acfun  7206
  Copyright terms: Public domain W3C validator