Description: Equivalence of the Axiom of Choice (first form) of Enderton p. 49 and our Axiom of Choice (in the form of ac2 ). The proof does not depend on AC but does depend on the Axiom of Regularity. (Contributed by Mario Carneiro, 17-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfac7 | |- ( CHOICE <-> A. x E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfac2 | |- ( CHOICE <-> A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) ) |
|
| 2 | aceq2 | |- ( E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) ) |
|
| 3 | 2 | albii | |- ( A. x E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) ) |
| 4 | 1 3 | bitr4i | |- ( CHOICE <-> A. x E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) ) |