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

Theorem zfcndac 9041
Description: Axiom of Choice ax-ac 8886, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
zfcndac  |-  E. y A. z A. w ( ( z  e.  w  /\  w  e.  x
)  ->  E. v A. u ( E. t
( ( u  e.  w  /\  w  e.  t )  /\  (
u  e.  t  /\  t  e.  y )
)  <->  u  =  v
) )
Distinct variable group:    x, y, z, w, v, u, t

Proof of Theorem zfcndac
StepHypRef Expression
1 axacnd 9034 . . 3  |-  E. y A. z A. w ( A. y ( 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 ) )
2 19.3v 1812 . . . . . 6  |-  ( A. y ( z  e.  w  /\  w  e.  x )  <->  ( z  e.  w  /\  w  e.  x ) )
32imbi1i 327 . . . . 5  |-  ( ( A. y ( 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 ) ) )
432albii 1691 . . . 4  |-  ( A. z A. w ( A. y ( 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 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 ) ) )
54exbii 1717 . . 3  |-  ( E. y A. z A. w ( A. y
( 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 ) )  <->  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 ) ) )
61, 5mpbi 212 . 2  |-  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 ) )
7 equequ2 1867 . . . . . . . . . 10  |-  ( v  =  x  ->  (
u  =  v  <->  u  =  x ) )
87bibi2d 320 . . . . . . . . 9  |-  ( v  =  x  ->  (
( E. t ( ( u  e.  w  /\  w  e.  t
)  /\  ( u  e.  t  /\  t  e.  y ) )  <->  u  =  v )  <->  ( E. t ( ( u  e.  w  /\  w  e.  t )  /\  (
u  e.  t  /\  t  e.  y )
)  <->  u  =  x
) ) )
9 elequ2 1900 . . . . . . . . . . . . 13  |-  ( t  =  x  ->  (
w  e.  t  <->  w  e.  x ) )
109anbi2d 709 . . . . . . . . . . . 12  |-  ( t  =  x  ->  (
( u  e.  w  /\  w  e.  t
)  <->  ( u  e.  w  /\  w  e.  x ) ) )
11 elequ2 1900 . . . . . . . . . . . . 13  |-  ( t  =  x  ->  (
u  e.  t  <->  u  e.  x ) )
12 elequ1 1893 . . . . . . . . . . . . 13  |-  ( t  =  x  ->  (
t  e.  y  <->  x  e.  y ) )
1311, 12anbi12d 716 . . . . . . . . . . . 12  |-  ( t  =  x  ->  (
( u  e.  t  /\  t  e.  y )  <->  ( u  e.  x  /\  x  e.  y ) ) )
1410, 13anbi12d 716 . . . . . . . . . . 11  |-  ( t  =  x  ->  (
( ( u  e.  w  /\  w  e.  t )  /\  (
u  e.  t  /\  t  e.  y )
)  <->  ( ( u  e.  w  /\  w  e.  x )  /\  (
u  e.  x  /\  x  e.  y )
) ) )
1514cbvexv 2116 . . . . . . . . . 10  |-  ( E. t ( ( u  e.  w  /\  w  e.  t )  /\  (
u  e.  t  /\  t  e.  y )
)  <->  E. x ( ( u  e.  w  /\  w  e.  x )  /\  ( u  e.  x  /\  x  e.  y
) ) )
1615bibi1i 316 . . . . . . . . 9  |-  ( ( E. t ( ( u  e.  w  /\  w  e.  t )  /\  ( u  e.  t  /\  t  e.  y ) )  <->  u  =  x )  <->  ( E. x ( ( u  e.  w  /\  w  e.  x )  /\  (
u  e.  x  /\  x  e.  y )
)  <->  u  =  x
) )
178, 16syl6bb 265 . . . . . . . 8  |-  ( v  =  x  ->  (
( E. t ( ( u  e.  w  /\  w  e.  t
)  /\  ( u  e.  t  /\  t  e.  y ) )  <->  u  =  v )  <->  ( E. x ( ( u  e.  w  /\  w  e.  x )  /\  (
u  e.  x  /\  x  e.  y )
)  <->  u  =  x
) ) )
1817albidv 1766 . . . . . . 7  |-  ( v  =  x  ->  ( A. u ( E. t
( ( u  e.  w  /\  w  e.  t )  /\  (
u  e.  t  /\  t  e.  y )
)  <->  u  =  v
)  <->  A. u ( E. x ( ( u  e.  w  /\  w  e.  x )  /\  (
u  e.  x  /\  x  e.  y )
)  <->  u  =  x
) ) )
19 elequ1 1893 . . . . . . . . . . . 12  |-  ( u  =  z  ->  (
u  e.  w  <->  z  e.  w ) )
2019anbi1d 710 . . . . . . . . . . 11  |-  ( u  =  z  ->  (
( u  e.  w  /\  w  e.  x
)  <->  ( z  e.  w  /\  w  e.  x ) ) )
21 elequ1 1893 . . . . . . . . . . . 12  |-  ( u  =  z  ->  (
u  e.  x  <->  z  e.  x ) )
2221anbi1d 710 . . . . . . . . . . 11  |-  ( u  =  z  ->  (
( u  e.  x  /\  x  e.  y
)  <->  ( z  e.  x  /\  x  e.  y ) ) )
2320, 22anbi12d 716 . . . . . . . . . 10  |-  ( u  =  z  ->  (
( ( u  e.  w  /\  w  e.  x )  /\  (
u  e.  x  /\  x  e.  y )
)  <->  ( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
) ) )
2423exbidv 1767 . . . . . . . . 9  |-  ( u  =  z  ->  ( E. x ( ( u  e.  w  /\  w  e.  x )  /\  (
u  e.  x  /\  x  e.  y )
)  <->  E. x ( ( z  e.  w  /\  w  e.  x )  /\  ( z  e.  x  /\  x  e.  y
) ) ) )
25 equequ1 1866 . . . . . . . . 9  |-  ( u  =  z  ->  (
u  =  x  <->  z  =  x ) )
2624, 25bibi12d 323 . . . . . . . 8  |-  ( u  =  z  ->  (
( E. x ( ( u  e.  w  /\  w  e.  x
)  /\  ( u  e.  x  /\  x  e.  y ) )  <->  u  =  x )  <->  ( E. x ( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) )
2726cbvalv 2115 . . . . . . 7  |-  ( A. u ( E. x
( ( u  e.  w  /\  w  e.  x )  /\  (
u  e.  x  /\  x  e.  y )
)  <->  u  =  x
)  <->  A. z ( E. x ( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) )
2818, 27syl6bb 265 . . . . . 6  |-  ( v  =  x  ->  ( A. u ( E. t
( ( u  e.  w  /\  w  e.  t )  /\  (
u  e.  t  /\  t  e.  y )
)  <->  u  =  v
)  <->  A. z ( E. x ( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) ) )
2928cbvexv 2116 . . . . 5  |-  ( E. v A. u ( E. t ( ( u  e.  w  /\  w  e.  t )  /\  ( u  e.  t  /\  t  e.  y ) )  <->  u  =  v )  <->  E. x A. z ( E. x
( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x ) )
3029imbi2i 314 . . . 4  |-  ( ( ( z  e.  w  /\  w  e.  x
)  ->  E. v A. u ( E. t
( ( u  e.  w  /\  w  e.  t )  /\  (
u  e.  t  /\  t  e.  y )
)  <->  u  =  v
) )  <->  ( (
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 ) ) )
31302albii 1691 . . 3  |-  ( A. z A. w ( ( z  e.  w  /\  w  e.  x )  ->  E. v A. u
( E. t ( ( u  e.  w  /\  w  e.  t
)  /\  ( u  e.  t  /\  t  e.  y ) )  <->  u  =  v ) )  <->  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 ) ) )
3231exbii 1717 . 2  |-  ( E. y A. z A. w ( ( z  e.  w  /\  w  e.  x )  ->  E. v A. u ( E. t
( ( u  e.  w  /\  w  e.  t )  /\  (
u  e.  t  /\  t  e.  y )
)  <->  u  =  v
) )  <->  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 ) ) )
336, 32mpbir 213 1  |-  E. y A. z A. w ( ( z  e.  w  /\  w  e.  x
)  ->  E. v A. u ( E. t
( ( u  e.  w  /\  w  e.  t )  /\  (
u  e.  t  /\  t  e.  y )
)  <->  u  =  v
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371   A.wal 1441    = wceq 1443   E.wex 1662    e. wcel 1886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638  ax-reg 8104  ax-ac 8886
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-opab 4461  df-eprel 4744  df-fr 4792
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator