This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )