MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  aceq1 Unicode version

Theorem aceq1 7744
Description: Equivalence of two versions of the Axiom of Choice ax-ac 8085. The proof uses neither AC nor the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables. (Contributed by NM, 5-Apr-2004.)
Assertion
Ref Expression
aceq1  |-  ( 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 A. w ( ( z  e.  w  /\  w  e.  x
)  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) )
Distinct variable group:    x, y, z, w, v, u

Proof of Theorem aceq1
Dummy variables  t  h are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 biidd 228 . . . . . . 7  |-  ( w  =  t  ->  ( E! v  e.  h  E. u  e.  y 
( h  e.  u  /\  v  e.  u
)  <->  E! v  e.  h  E. u  e.  y 
( h  e.  u  /\  v  e.  u
) ) )
21cbvralv 2764 . . . . . 6  |-  ( A. w  e.  h  E! v  e.  h  E. u  e.  y  (
h  e.  u  /\  v  e.  u )  <->  A. t  e.  h  E! v  e.  h  E. u  e.  y  (
h  e.  u  /\  v  e.  u )
)
3 eleq1 2343 . . . . . . . . . 10  |-  ( v  =  z  ->  (
v  e.  u  <->  z  e.  u ) )
43anbi2d 684 . . . . . . . . 9  |-  ( v  =  z  ->  (
( h  e.  u  /\  v  e.  u
)  <->  ( h  e.  u  /\  z  e.  u ) ) )
54rexbidv 2564 . . . . . . . 8  |-  ( v  =  z  ->  ( E. u  e.  y 
( h  e.  u  /\  v  e.  u
)  <->  E. u  e.  y  ( h  e.  u  /\  z  e.  u
) ) )
65cbvreuv 2766 . . . . . . 7  |-  ( E! v  e.  h  E. u  e.  y  (
h  e.  u  /\  v  e.  u )  <->  E! z  e.  h  E. u  e.  y  (
h  e.  u  /\  z  e.  u )
)
76ralbii 2567 . . . . . 6  |-  ( A. t  e.  h  E! v  e.  h  E. u  e.  y  (
h  e.  u  /\  v  e.  u )  <->  A. t  e.  h  E! z  e.  h  E. u  e.  y  (
h  e.  u  /\  z  e.  u )
)
82, 7bitri 240 . . . . 5  |-  ( A. w  e.  h  E! v  e.  h  E. u  e.  y  (
h  e.  u  /\  v  e.  u )  <->  A. t  e.  h  E! z  e.  h  E. u  e.  y  (
h  e.  u  /\  z  e.  u )
)
98ralbii 2567 . . . 4  |-  ( A. h  e.  x  A. w  e.  h  E! v  e.  h  E. u  e.  y  (
h  e.  u  /\  v  e.  u )  <->  A. h  e.  x  A. t  e.  h  E! z  e.  h  E. u  e.  y  (
h  e.  u  /\  z  e.  u )
)
10 eleq1 2343 . . . . . . . . 9  |-  ( z  =  h  ->  (
z  e.  u  <->  h  e.  u ) )
1110anbi1d 685 . . . . . . . 8  |-  ( z  =  h  ->  (
( z  e.  u  /\  v  e.  u
)  <->  ( h  e.  u  /\  v  e.  u ) ) )
1211rexbidv 2564 . . . . . . 7  |-  ( z  =  h  ->  ( E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  <->  E. u  e.  y  ( h  e.  u  /\  v  e.  u
) ) )
1312reueqd 2746 . . . . . 6  |-  ( z  =  h  ->  ( E! v  e.  z  E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  <->  E! v  e.  h  E. u  e.  y 
( h  e.  u  /\  v  e.  u
) ) )
1413raleqbi1dv 2744 . . . . 5  |-  ( z  =  h  ->  ( A. w  e.  z  E! v  e.  z  E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  <->  A. w  e.  h  E! v  e.  h  E. u  e.  y 
( h  e.  u  /\  v  e.  u
) ) )
1514cbvralv 2764 . . . 4  |-  ( A. z  e.  x  A. w  e.  z  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  <->  A. h  e.  x  A. w  e.  h  E! v  e.  h  E. u  e.  y  (
h  e.  u  /\  v  e.  u )
)
16 eleq1 2343 . . . . . . . . 9  |-  ( w  =  h  ->  (
w  e.  u  <->  h  e.  u ) )
1716anbi1d 685 . . . . . . . 8  |-  ( w  =  h  ->  (
( w  e.  u  /\  z  e.  u
)  <->  ( h  e.  u  /\  z  e.  u ) ) )
1817rexbidv 2564 . . . . . . 7  |-  ( w  =  h  ->  ( E. u  e.  y 
( w  e.  u  /\  z  e.  u
)  <->  E. u  e.  y  ( h  e.  u  /\  z  e.  u
) ) )
1918reueqd 2746 . . . . . 6  |-  ( w  =  h  ->  ( E! z  e.  w  E. u  e.  y 
( w  e.  u  /\  z  e.  u
)  <->  E! z  e.  h  E. u  e.  y 
( h  e.  u  /\  z  e.  u
) ) )
2019raleqbi1dv 2744 . . . . 5  |-  ( w  =  h  ->  ( A. t  e.  w  E! z  e.  w  E. u  e.  y 
( w  e.  u  /\  z  e.  u
)  <->  A. t  e.  h  E! z  e.  h  E. u  e.  y 
( h  e.  u  /\  z  e.  u
) ) )
2120cbvralv 2764 . . . 4  |-  ( A. w  e.  x  A. t  e.  w  E! z  e.  w  E. u  e.  y  (
w  e.  u  /\  z  e.  u )  <->  A. h  e.  x  A. t  e.  h  E! z  e.  h  E. u  e.  y  (
h  e.  u  /\  z  e.  u )
)
229, 15, 213bitr4i 268 . . 3  |-  ( A. z  e.  x  A. w  e.  z  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  <->  A. w  e.  x  A. t  e.  w  E! z  e.  w  E. u  e.  y  (
w  e.  u  /\  z  e.  u )
)
2322exbii 1569 . 2  |-  ( 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. w  e.  x  A. t  e.  w  E! z  e.  w  E. u  e.  y 
( w  e.  u  /\  z  e.  u
) )
24 19.21v 1831 . . . . . 6  |-  ( A. z ( w  e.  x  ->  ( z  e.  w  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) )  <->  ( w  e.  x  ->  A. z
( z  e.  w  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) ) ) )
25 impexp 433 . . . . . . . 8  |-  ( ( ( z  e.  w  /\  w  e.  x
)  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) )  <->  ( z  e.  w  ->  ( w  e.  x  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) ) )
26 bi2.04 350 . . . . . . . 8  |-  ( ( z  e.  w  -> 
( w  e.  x  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) ) )  <-> 
( w  e.  x  ->  ( z  e.  w  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) ) ) )
2725, 26bitri 240 . . . . . . 7  |-  ( ( ( z  e.  w  /\  w  e.  x
)  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) )  <->  ( w  e.  x  ->  ( z  e.  w  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) ) )
2827albii 1553 . . . . . 6  |-  ( A. z ( ( z  e.  w  /\  w  e.  x )  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) )  <->  A. z
( w  e.  x  ->  ( z  e.  w  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) ) ) )
29 df-eu 2147 . . . . . . . . . . 11  |-  ( E! z ( z  e.  w  /\  E. u  e.  y  ( w  e.  u  /\  z  e.  u ) )  <->  E. x A. z ( ( z  e.  w  /\  E. u  e.  y  (
w  e.  u  /\  z  e.  u )
)  <->  z  =  x ) )
30 df-reu 2550 . . . . . . . . . . 11  |-  ( E! z  e.  w  E. u  e.  y  (
w  e.  u  /\  z  e.  u )  <->  E! z ( z  e.  w  /\  E. u  e.  y  ( w  e.  u  /\  z  e.  u ) ) )
31 19.42v 1846 . . . . . . . . . . . . . . 15  |-  ( E. x ( z  e.  w  /\  ( x  e.  y  /\  (
w  e.  x  /\  z  e.  x )
) )  <->  ( z  e.  w  /\  E. x
( x  e.  y  /\  ( w  e.  x  /\  z  e.  x ) ) ) )
32 an42 798 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z  e.  w  /\  x  e.  y
)  /\  ( w  e.  x  /\  z  e.  x ) )  <->  ( (
z  e.  w  /\  w  e.  x )  /\  ( z  e.  x  /\  x  e.  y
) ) )
33 anass 630 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z  e.  w  /\  x  e.  y
)  /\  ( w  e.  x  /\  z  e.  x ) )  <->  ( z  e.  w  /\  (
x  e.  y  /\  ( w  e.  x  /\  z  e.  x
) ) ) )
3432, 33bitr3i 242 . . . . . . . . . . . . . . . 16  |-  ( ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  ( z  e.  w  /\  (
x  e.  y  /\  ( w  e.  x  /\  z  e.  x
) ) ) )
3534exbii 1569 . . . . . . . . . . . . . . 15  |-  ( E. x ( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  E. x ( z  e.  w  /\  (
x  e.  y  /\  ( w  e.  x  /\  z  e.  x
) ) ) )
36 df-rex 2549 . . . . . . . . . . . . . . . . 17  |-  ( E. u  e.  y  ( w  e.  u  /\  z  e.  u )  <->  E. u ( u  e.  y  /\  ( w  e.  u  /\  z  e.  u ) ) )
37 eleq1 2343 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  x  ->  (
u  e.  y  <->  x  e.  y ) )
38 eleq2 2344 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  x  ->  (
w  e.  u  <->  w  e.  x ) )
39 eleq2 2344 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  x  ->  (
z  e.  u  <->  z  e.  x ) )
4038, 39anbi12d 691 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  x  ->  (
( w  e.  u  /\  z  e.  u
)  <->  ( w  e.  x  /\  z  e.  x ) ) )
4137, 40anbi12d 691 . . . . . . . . . . . . . . . . . 18  |-  ( u  =  x  ->  (
( u  e.  y  /\  ( w  e.  u  /\  z  e.  u ) )  <->  ( x  e.  y  /\  (
w  e.  x  /\  z  e.  x )
) ) )
4241cbvexv 1943 . . . . . . . . . . . . . . . . 17  |-  ( E. u ( u  e.  y  /\  ( w  e.  u  /\  z  e.  u ) )  <->  E. x
( x  e.  y  /\  ( w  e.  x  /\  z  e.  x ) ) )
4336, 42bitri 240 . . . . . . . . . . . . . . . 16  |-  ( E. u  e.  y  ( w  e.  u  /\  z  e.  u )  <->  E. x ( x  e.  y  /\  ( w  e.  x  /\  z  e.  x ) ) )
4443anbi2i 675 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  w  /\  E. u  e.  y  ( w  e.  u  /\  z  e.  u )
)  <->  ( z  e.  w  /\  E. x
( x  e.  y  /\  ( w  e.  x  /\  z  e.  x ) ) ) )
4531, 35, 443bitr4i 268 . . . . . . . . . . . . . 14  |-  ( E. x ( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  ( z  e.  w  /\  E. u  e.  y  ( w  e.  u  /\  z  e.  u ) ) )
4645bibi1i 305 . . . . . . . . . . . . 13  |-  ( ( E. x ( ( z  e.  w  /\  w  e.  x )  /\  ( z  e.  x  /\  x  e.  y
) )  <->  z  =  x )  <->  ( (
z  e.  w  /\  E. u  e.  y  ( w  e.  u  /\  z  e.  u )
)  <->  z  =  x ) )
4746albii 1553 . . . . . . . . . . . 12  |-  ( A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x )  <->  A. z ( ( z  e.  w  /\  E. u  e.  y  ( w  e.  u  /\  z  e.  u )
)  <->  z  =  x ) )
4847exbii 1569 . . . . . . . . . . 11  |-  ( E. x A. z ( E. x ( ( z  e.  w  /\  w  e.  x )  /\  ( z  e.  x  /\  x  e.  y
) )  <->  z  =  x )  <->  E. x A. z ( ( z  e.  w  /\  E. u  e.  y  (
w  e.  u  /\  z  e.  u )
)  <->  z  =  x ) )
4929, 30, 483bitr4i 268 . . . . . . . . . 10  |-  ( E! z  e.  w  E. u  e.  y  (
w  e.  u  /\  z  e.  u )  <->  E. x A. z ( E. x ( ( z  e.  w  /\  w  e.  x )  /\  ( z  e.  x  /\  x  e.  y
) )  <->  z  =  x ) )
5049imbi2i 303 . . . . . . . . 9  |-  ( ( t  e.  w  ->  E! z  e.  w  E. u  e.  y 
( w  e.  u  /\  z  e.  u
) )  <->  ( t  e.  w  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) )
5150albii 1553 . . . . . . . 8  |-  ( A. t ( t  e.  w  ->  E! z  e.  w  E. u  e.  y  ( w  e.  u  /\  z  e.  u ) )  <->  A. t
( t  e.  w  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) ) )
52 df-ral 2548 . . . . . . . 8  |-  ( A. t  e.  w  E! z  e.  w  E. u  e.  y  (
w  e.  u  /\  z  e.  u )  <->  A. t ( t  e.  w  ->  E! z  e.  w  E. u  e.  y  ( w  e.  u  /\  z  e.  u ) ) )
53 nfv 1605 . . . . . . . . 9  |-  F/ t ( z  e.  w  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) )
54 nfv 1605 . . . . . . . . . 10  |-  F/ z  t  e.  w
55 nfa1 1756 . . . . . . . . . . 11  |-  F/ z A. z ( E. x ( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x )
5655nfex 1767 . . . . . . . . . 10  |-  F/ z E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x )
5754, 56nfim 1769 . . . . . . . . 9  |-  F/ z ( t  e.  w  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) )
58 eleq1 2343 . . . . . . . . . 10  |-  ( z  =  t  ->  (
z  e.  w  <->  t  e.  w ) )
5958imbi1d 308 . . . . . . . . 9  |-  ( z  =  t  ->  (
( z  e.  w  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) )  <->  ( t  e.  w  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) ) )
6053, 57, 59cbval 1924 . . . . . . . 8  |-  ( A. z ( z  e.  w  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) )  <->  A. t
( t  e.  w  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) ) )
6151, 52, 603bitr4i 268 . . . . . . 7  |-  ( A. t  e.  w  E! z  e.  w  E. u  e.  y  (
w  e.  u  /\  z  e.  u )  <->  A. z ( z  e.  w  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) )
6261imbi2i 303 . . . . . 6  |-  ( ( w  e.  x  ->  A. t  e.  w  E! z  e.  w  E. u  e.  y 
( w  e.  u  /\  z  e.  u
) )  <->  ( w  e.  x  ->  A. z
( z  e.  w  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) ) ) )
6324, 28, 623bitr4i 268 . . . . 5  |-  ( A. z ( ( z  e.  w  /\  w  e.  x )  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) )  <->  ( w  e.  x  ->  A. t  e.  w  E! z  e.  w  E. u  e.  y  ( w  e.  u  /\  z  e.  u ) ) )
6463albii 1553 . . . 4  |-  ( A. w A. z ( ( z  e.  w  /\  w  e.  x )  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) )  <->  A. w
( w  e.  x  ->  A. t  e.  w  E! z  e.  w  E. u  e.  y 
( w  e.  u  /\  z  e.  u
) ) )
65 alcom 1711 . . . 4  |-  ( A. z A. w ( ( z  e.  w  /\  w  e.  x )  ->  E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x ) )  <->  A. w A. z ( ( z  e.  w  /\  w  e.  x )  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) )
66 df-ral 2548 . . . 4  |-  ( A. w  e.  x  A. t  e.  w  E! z  e.  w  E. u  e.  y  (
w  e.  u  /\  z  e.  u )  <->  A. w ( w  e.  x  ->  A. t  e.  w  E! z  e.  w  E. u  e.  y  ( w  e.  u  /\  z  e.  u ) ) )
6764, 65, 663bitr4ri 269 . . 3  |-  ( A. w  e.  x  A. t  e.  w  E! z  e.  w  E. u  e.  y  (
w  e.  u  /\  z  e.  u )  <->  A. z A. w ( ( z  e.  w  /\  w  e.  x
)  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) )
6867exbii 1569 . 2  |-  ( E. y A. w  e.  x  A. t  e.  w  E! z  e.  w  E. u  e.  y  ( w  e.  u  /\  z  e.  u )  <->  E. y A. z A. w ( ( z  e.  w  /\  w  e.  x
)  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) )
6923, 68bitri 240 1  |-  ( 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 A. w ( ( z  e.  w  /\  w  e.  x
)  ->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684   E!weu 2143   A.wral 2543   E.wrex 2544   E!wreu 2545
This theorem is referenced by:  aceq0  7745  dfac1  7760
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-reu 2550
  Copyright terms: Public domain W3C validator