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

Theorem pwex 4193
Description: Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Hypothesis
Ref Expression
zfpowcl.1  |-  A  e. 
_V
Assertion
Ref Expression
pwex  |-  ~P A  e.  _V

Proof of Theorem pwex
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zfpowcl.1 . 2  |-  A  e. 
_V
2 pweq 3628 . . 3  |-  ( z  =  A  ->  ~P z  =  ~P A
)
32eleq1d 2349 . 2  |-  ( z  =  A  ->  ( ~P z  e.  _V  <->  ~P A  e.  _V )
)
4 df-pw 3627 . . 3  |-  ~P z  =  { y  |  y 
C_  z }
5 axpow2 4190 . . . . . 6  |-  E. x A. y ( y  C_  z  ->  y  e.  x
)
65bm1.3ii 4144 . . . . 5  |-  E. x A. y ( y  e.  x  <->  y  C_  z
)
7 abeq2 2388 . . . . . 6  |-  ( x  =  { y  |  y  C_  z }  <->  A. y ( y  e.  x  <->  y  C_  z
) )
87exbii 1569 . . . . 5  |-  ( E. x  x  =  {
y  |  y  C_  z }  <->  E. x A. y
( y  e.  x  <->  y 
C_  z ) )
96, 8mpbir 200 . . . 4  |-  E. x  x  =  { y  |  y  C_  z }
109issetri 2795 . . 3  |-  { y  |  y  C_  z }  e.  _V
114, 10eqeltri 2353 . 2  |-  ~P z  e.  _V
121, 3, 11vtocl 2838 1  |-  ~P A  e.  _V
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684   {cab 2269   _Vcvv 2788    C_ wss 3152   ~Pcpw 3625
This theorem is referenced by:  pwexg  4194  p0ex  4197  pp0ex  4199  ord3ex  4200  abexssex  5781  fnpm  6780  canth2  7014  dffi3  7184  inf3lem7  7335  r1sucg  7441  r1pwOLD  7518  rankuni  7535  rankc2  7543  rankxpu  7548  rankxplim  7549  r0weon  7640  aceq3lem  7747  dfac5lem4  7753  dfac2a  7756  dfac2  7757  dfac8  7761  dfac13  7768  ackbij1lem5  7850  ackbij1lem8  7853  ackbij2lem2  7866  ackbij2lem3  7867  fin23lem17  7964  domtriomlem  8068  dominf  8071  axdc2lem  8074  axdc3lem  8076  numthcor  8121  axdclem2  8147  alephsucpw  8192  dominfac  8195  canthp1lem1  8274  gchac  8295  intwun  8357  wunex2  8360  eltsk2g  8373  inttsk  8396  tskcard  8403  intgru  8436  gruina  8440  axgroth6  8450  npex  8610  axcnex  8769  pnfxr  10455  mnfxr  10456  ixxex  10667  prdsval  13355  prdsds  13363  prdshom  13366  ismre  13492  fnmre  13493  fnmrc  13509  mrcfval  13510  mrisval  13532  mreacs  13560  wunfunc  13773  catcfuccl  13941  catcxpccl  13981  lubfval  14112  glbfval  14117  isacs5lem  14272  issubm  14425  issubg  14621  cntzfval  14796  sylow1lem2  14910  lsmfval  14949  pj1fval  15003  issubrg  15545  lssset  15691  lspfval  15730  islbs  15829  lbsext  15916  lbsexg  15917  sraval  15929  aspval  16068  ocvfval  16566  cssval  16582  isobs  16620  istopon  16663  tgdom  16716  fncld  16759  leordtval2  16942  cnpfval  16964  iscnp2  16969  kgenf  17236  xkoopn  17284  xkouni  17294  dfac14  17312  xkoccn  17313  prdstopn  17322  xkoco1cn  17351  xkoco2cn  17352  xkococn  17354  xkoinjcn  17381  isfbas  17524  uzrest  17592  acufl  17612  alexsubALTlem2  17742  tsmsval2  17812  ishtpy  18470  vitali  18968  sspval  21299  shex  21791  hsupval  21913  ballotlemoex  23044  isrnsigaOLD  23473  dmvlsiga  23490  coinflippv  23684  kur14lem9  23745  idlvalNEW  25445  intvlset  25698  issubcat  25845  vtarsuelt  25895  isconcl1b  26097  heibor1lem  26533  heibor  26545  idlval  26638  mzpclval  26803  eldiophb  26836  rpnnen3  27125  dfac11  27160  islinds  27279  rgspnval  27373  pmtrfval  27393  psubspset  29933  paddfval  29986  pclfvalN  30078  polfvalN  30093  psubclsetN  30125  docafvalN  31312  djafvalN  31324  dicval  31366  dochfval  31540  djhfval  31587  islpolN  31673
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-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-pow 4188
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627
  Copyright terms: Public domain W3C validator