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

Definition df-ac 7143
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 4498 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 7142 . 2 wff CHOICE
2 vf . . . . . . 7 setvar 𝑓
32cv 1334 . . . . . 6 class 𝑓
4 vx . . . . . . 7 setvar 𝑥
54cv 1334 . . . . . 6 class 𝑥
63, 5wss 3102 . . . . 5 wff 𝑓𝑥
75cdm 4588 . . . . . 6 class dom 𝑥
83, 7wfn 5167 . . . . 5 wff 𝑓 Fn dom 𝑥
96, 8wa 103 . . . 4 wff (𝑓𝑥𝑓 Fn dom 𝑥)
109, 2wex 1472 . . 3 wff 𝑓(𝑓𝑥𝑓 Fn dom 𝑥)
1110, 4wal 1333 . 2 wff 𝑥𝑓(𝑓𝑥𝑓 Fn dom 𝑥)
121, 11wb 104 1 wff (CHOICE ↔ ∀𝑥𝑓(𝑓𝑥𝑓 Fn dom 𝑥))
Colors of variables: wff set class
This definition is referenced by:  acfun  7144
  Copyright terms: Public domain W3C validator