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

Theorem aceq1 7931
Description: Equivalence of two versions of the Axiom of Choice ax-ac 8272. 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 229 . . . . . . 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 2875 . . . . . 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 2447 . . . . . . . . . 10  |-  ( v  =  z  ->  (
v  e.  u  <->  z  e.  u ) )
43anbi2d 685 . . . . . . . . 9  |-  ( v  =  z  ->  (
( h  e.  u  /\  v  e.  u
)  <->  ( h  e.  u  /\  z  e.  u ) ) )
54rexbidv 2670 . . . . . . . 8  |-  ( v  =  z  ->  ( E. u  e.  y 
( h  e.  u  /\  v  e.  u
)  <->  E. u  e.  y  ( h  e.  u  /\  z  e.  u
) ) )
65cbvreuv 2877 . . . . . . 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 2673 . . . . . 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 241 . . . . 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 2673 . . . 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 2447 . . . . . . . . 9  |-  ( z  =  h  ->  (
z  e.  u  <->  h  e.  u ) )
1110anbi1d 686 . . . . . . . 8  |-  ( z  =  h  ->  (
( z  e.  u  /\  v  e.  u
)  <->  ( h  e.  u  /\  v  e.  u ) ) )
1211rexbidv 2670 . . . . . . 7  |-  ( z  =  h  ->  ( E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  <->  E. u  e.  y  ( h  e.  u  /\  v  e.  u
) ) )
1312reueqd 2857 . . . . . 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 2855 . . . . 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 2875 . . . 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 2447 . . . . . . . . 9  |-  ( w  =  h  ->  (
w  e.  u  <->  h  e.  u ) )
1716anbi1d 686 . . . . . . . 8  |-  ( w  =  h  ->  (
( w  e.  u  /\  z  e.  u
)  <->  ( h  e.  u  /\  z  e.  u ) ) )
1817rexbidv 2670 . . . . . . 7  |-  ( w  =  h  ->  ( E. u  e.  y 
( w  e.  u  /\  z  e.  u
)  <->  E. u  e.  y  ( h  e.  u  /\  z  e.  u
) ) )
1918reueqd 2857 . . . . . 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 2855 . . . . 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 2875 . . . 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 269 . . 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 1589 . 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 1902 . . . . . 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 434 . . . . . . . 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 351 . . . . . . . 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 241 . . . . . . 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 1572 . . . . . 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 2242 . . . . . . . . . . 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 2656 . . . . . . . . . . 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 1917 . . . . . . . . . . . . . . 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 799 . . . . . . . . . . . . . . . . 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 631 . . . . . . . . . . . . . . . . 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 243 . . . . . . . . . . . . . . . 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 1589 . . . . . . . . . . . . . . 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 2655 . . . . . . . . . . . . . . . . 17  |-  ( E. u  e.  y  ( w  e.  u  /\  z  e.  u )  <->  E. u ( u  e.  y  /\  ( w  e.  u  /\  z  e.  u ) ) )
37 eleq1 2447 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  x  ->  (
u  e.  y  <->  x  e.  y ) )
38 eleq2 2448 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  x  ->  (
w  e.  u  <->  w  e.  x ) )
39 eleq2 2448 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  x  ->  (
z  e.  u  <->  z  e.  x ) )
4038, 39anbi12d 692 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  x  ->  (
( w  e.  u  /\  z  e.  u
)  <->  ( w  e.  x  /\  z  e.  x ) ) )
4137, 40anbi12d 692 . . . . . . . . . . . . . . . . . 18  |-  ( u  =  x  ->  (
( u  e.  y  /\  ( w  e.  u  /\  z  e.  u ) )  <->  ( x  e.  y  /\  (
w  e.  x  /\  z  e.  x )
) ) )
4241cbvexv 2037 . . . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . . . . . 16  |-  ( E. u  e.  y  ( w  e.  u  /\  z  e.  u )  <->  E. x ( x  e.  y  /\  ( w  e.  x  /\  z  e.  x ) ) )
4443anbi2i 676 . . . . . . . . . . . . . . 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 269 . . . . . . . . . . . . . 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 306 . . . . . . . . . . . . 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 1572 . . . . . . . . . . . 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 1589 . . . . . . . . . . 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 269 . . . . . . . . . 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 304 . . . . . . . . 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 1572 . . . . . . . 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 2654 . . . . . . . 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 1626 . . . . . . . . 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 1626 . . . . . . . . . 10  |-  F/ z  t  e.  w
55 nfa1 1796 . . . . . . . . . . 11  |-  F/ z A. z ( E. x ( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x )
5655nfex 1855 . . . . . . . . . 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 1822 . . . . . . . . 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 2447 . . . . . . . . . 10  |-  ( z  =  t  ->  (
z  e.  w  <->  t  e.  w ) )
5958imbi1d 309 . . . . . . . . 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 2019 . . . . . . . 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 269 . . . . . . 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 304 . . . . . 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 269 . . . . 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 1572 . . . 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 1744 . . . 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 2654 . . . 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 270 . . 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 1589 . 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 241 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 177    /\ wa 359   A.wal 1546   E.wex 1547   E!weu 2238   A.wral 2649   E.wrex 2650   E!wreu 2651
This theorem is referenced by:  aceq0  7932  dfac1  7947
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-rex 2655  df-reu 2656
  Copyright terms: Public domain W3C validator