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

Theorem zfcndac 8900
Description: Axiom of Choice ax-ac 8742, 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 8893 . . 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 nfv 1674 . . . . . . 7  |-  F/ y ( z  e.  w  /\  w  e.  x
)
3219.3 1827 . . . . . 6  |-  ( A. y ( z  e.  w  /\  w  e.  x )  <->  ( z  e.  w  /\  w  e.  x ) )
43imbi1i 325 . . . . 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 ) ) )
542albii 1612 . . . 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 ) ) )
65exbii 1635 . . 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 ) ) )
71, 6mpbi 208 . 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 ) )
8 equequ2 1739 . . . . . . . . . 10  |-  ( v  =  x  ->  (
u  =  v  <->  u  =  x ) )
98bibi2d 318 . . . . . . . . 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
) ) )
10 elequ2 1763 . . . . . . . . . . . . 13  |-  ( t  =  x  ->  (
w  e.  t  <->  w  e.  x ) )
1110anbi2d 703 . . . . . . . . . . . 12  |-  ( t  =  x  ->  (
( u  e.  w  /\  w  e.  t
)  <->  ( u  e.  w  /\  w  e.  x ) ) )
12 elequ2 1763 . . . . . . . . . . . . 13  |-  ( t  =  x  ->  (
u  e.  t  <->  u  e.  x ) )
13 elequ1 1761 . . . . . . . . . . . . 13  |-  ( t  =  x  ->  (
t  e.  y  <->  x  e.  y ) )
1412, 13anbi12d 710 . . . . . . . . . . . 12  |-  ( t  =  x  ->  (
( u  e.  t  /\  t  e.  y )  <->  ( u  e.  x  /\  x  e.  y ) ) )
1511, 14anbi12d 710 . . . . . . . . . . 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 )
) ) )
1615cbvexv 1984 . . . . . . . . . 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
) ) )
1716bibi1i 314 . . . . . . . . 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
) )
189, 17syl6bb 261 . . . . . . . 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
) ) )
1918albidv 1680 . . . . . . 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
) ) )
20 elequ1 1761 . . . . . . . . . . . 12  |-  ( u  =  z  ->  (
u  e.  w  <->  z  e.  w ) )
2120anbi1d 704 . . . . . . . . . . 11  |-  ( u  =  z  ->  (
( u  e.  w  /\  w  e.  x
)  <->  ( z  e.  w  /\  w  e.  x ) ) )
22 elequ1 1761 . . . . . . . . . . . 12  |-  ( u  =  z  ->  (
u  e.  x  <->  z  e.  x ) )
2322anbi1d 704 . . . . . . . . . . 11  |-  ( u  =  z  ->  (
( u  e.  x  /\  x  e.  y
)  <->  ( z  e.  x  /\  x  e.  y ) ) )
2421, 23anbi12d 710 . . . . . . . . . 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 )
) ) )
2524exbidv 1681 . . . . . . . . 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
) ) ) )
26 equequ1 1738 . . . . . . . . 9  |-  ( u  =  z  ->  (
u  =  x  <->  z  =  x ) )
2725, 26bibi12d 321 . . . . . . . 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 ) ) )
2827cbvalv 1983 . . . . . . 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 ) )
2919, 28syl6bb 261 . . . . . 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 ) ) )
3029cbvexv 1984 . . . . 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 ) )
3130imbi2i 312 . . . 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 ) ) )
32312albii 1612 . . 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 ) ) )
3332exbii 1635 . 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 ) ) )
347, 33mpbir 209 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 184    /\ wa 369   A.wal 1368    = wceq 1370   E.wex 1587    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642  ax-reg 7921  ax-ac 8742
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-br 4404  df-opab 4462  df-eprel 4743  df-fr 4790
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator