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

Definition df-ac 7183
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 4521 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 7182 . 2 wff CHOICE
2 vf . . . . . . 7 setvar 𝑓
32cv 1347 . . . . . 6 class 𝑓
4 vx . . . . . . 7 setvar 𝑥
54cv 1347 . . . . . 6 class 𝑥
63, 5wss 3121 . . . . 5 wff 𝑓𝑥
75cdm 4611 . . . . . 6 class dom 𝑥
83, 7wfn 5193 . . . . 5 wff 𝑓 Fn dom 𝑥
96, 8wa 103 . . . 4 wff (𝑓𝑥𝑓 Fn dom 𝑥)
109, 2wex 1485 . . 3 wff 𝑓(𝑓𝑥𝑓 Fn dom 𝑥)
1110, 4wal 1346 . 2 wff 𝑥𝑓(𝑓𝑥𝑓 Fn dom 𝑥)
121, 11wb 104 1 wff (CHOICE ↔ ∀𝑥𝑓(𝑓𝑥𝑓 Fn dom 𝑥))
Colors of variables: wff set class
This definition is referenced by:  acfun  7184
  Copyright terms: Public domain W3C validator