Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfac  Structured version Unicode version 
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 is a slight problem with taking the exact form of axac 8830 as our definition, because the equivalence to more standard forms (dfac2 8502) requires the Axiom of Regularity, which we often try to avoid. Thus, we take the first of the "textbook forms" as the definition and derive the form of axac 8830 itself as dfac0 8504. (Contributed by Mario Carneiro, 22Feb2015.) 
Ref  Expression 

dfac  CHOICE 
Step  Hyp  Ref  Expression 

1  wac 8487  . 2 CHOICE  
2  vf  . . . . . . 7  
3  2  cv 1397  . . . . . 6 
4  vx  . . . . . . 7  
5  4  cv 1397  . . . . . 6 
6  3, 5  wss 3461  . . . . 5 
7  5  cdm 4988  . . . . . 6 
8  3, 7  wfn 5565  . . . . 5 
9  6, 8  wa 367  . . . 4 
10  9, 2  wex 1617  . . 3 
11  10, 4  wal 1396  . 2 
12  1, 11  wb 184  1 CHOICE 
Colors of variables: wff setvar class 
This definition is referenced by: dfac3 8493 ac7 8844 
Copyright terms: Public domain  W3C validator 