Metamath Proof Explorer


Theorem aceq2

Description: Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. (Contributed by NM, 5-Apr-2004)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 df-ral
 |-  ( A. t e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> A. t ( t e. z -> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) )
2 19.23v
 |-  ( A. t ( t e. z -> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) <-> ( E. t t e. z -> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) )
3 1 2 bitri
 |-  ( A. t e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> ( E. t t e. z -> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) )
4 biidd
 |-  ( w = t -> ( E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) )
5 4 cbvralvw
 |-  ( A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> A. t e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) )
6 n0
 |-  ( z =/= (/) <-> E. t t e. z )
7 elequ2
 |-  ( v = u -> ( z e. v <-> z e. u ) )
8 elequ2
 |-  ( v = u -> ( w e. v <-> w e. u ) )
9 7 8 anbi12d
 |-  ( v = u -> ( ( z e. v /\ w e. v ) <-> ( z e. u /\ w e. u ) ) )
10 9 cbvrexvw
 |-  ( E. v e. y ( z e. v /\ w e. v ) <-> E. u e. y ( z e. u /\ w e. u ) )
11 10 reubii
 |-  ( E! w e. z E. v e. y ( z e. v /\ w e. v ) <-> E! w e. z E. u e. y ( z e. u /\ w e. u ) )
12 elequ1
 |-  ( w = v -> ( w e. u <-> v e. u ) )
13 12 anbi2d
 |-  ( w = v -> ( ( z e. u /\ w e. u ) <-> ( z e. u /\ v e. u ) ) )
14 13 rexbidv
 |-  ( w = v -> ( E. u e. y ( z e. u /\ w e. u ) <-> E. u e. y ( z e. u /\ v e. u ) ) )
15 14 cbvreuvw
 |-  ( E! w e. z E. u e. y ( z e. u /\ w e. u ) <-> E! v e. z E. u e. y ( z e. u /\ v e. u ) )
16 11 15 bitri
 |-  ( E! w e. z E. v e. y ( z e. v /\ w e. v ) <-> E! v e. z E. u e. y ( z e. u /\ v e. u ) )
17 6 16 imbi12i
 |-  ( ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) <-> ( E. t t e. z -> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) )
18 3 5 17 3bitr4i
 |-  ( A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
19 18 ralbii
 |-  ( A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
20 19 exbii
 |-  ( 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 ) ) )