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

Theorem pwex 4131
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
StepHypRef Expression
1 zfpowcl.1 . 2  |-  A  e. 
_V
2 pweq 3569 . . 3  |-  ( z  =  A  ->  ~P z  =  ~P A
)
32eleq1d 2322 . 2  |-  ( z  =  A  ->  ( ~P z  e.  _V  <->  ~P A  e.  _V )
)
4 df-pw 3568 . . 3  |-  ~P z  =  { y  |  y 
C_  z }
5 axpow2 4128 . . . . . 6  |-  E. x A. y ( y  C_  z  ->  y  e.  x
)
65bm1.3ii 4084 . . . . 5  |-  E. x A. y ( y  e.  x  <->  y  C_  z
)
7 abeq2 2361 . . . . . 6  |-  ( x  =  { y  |  y  C_  z }  <->  A. y ( y  e.  x  <->  y  C_  z
) )
87exbii 1580 . . . . 5  |-  ( E. x  x  =  {
y  |  y  C_  z }  <->  E. x A. y
( y  e.  x  <->  y 
C_  z ) )
96, 8mpbir 202 . . . 4  |-  E. x  x  =  { y  |  y  C_  z }
109issetri 2747 . . 3  |-  { y  |  y  C_  z }  e.  _V
114, 10eqeltri 2326 . 2  |-  ~P z  e.  _V
121, 3, 11vtocl 2789 1  |-  ~P A  e.  _V
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1532   E.wex 1537    = wceq 1619    e. wcel 1621   {cab 2242   _Vcvv 2740    C_ wss 3094   ~Pcpw 3566
This theorem is referenced by:  pwexg  4132  p0ex  4135  pp0ex  4137  ord3ex  4138  abexssex  5680  fnpm  6713  canth2  6947  dffi3  7117  inf3lem7  7268  r1sucg  7374  r1pwOLD  7451  rankuni  7468  rankc2  7476  rankxpu  7481  rankxplim  7482  r0weon  7573  aceq3lem  7680  dfac5lem4  7686  dfac2a  7689  dfac2  7690  dfac8  7694  dfac13  7701  ackbij1lem5  7783  ackbij1lem8  7786  ackbij2lem2  7799  ackbij2lem3  7800  fin23lem17  7897  domtriomlem  8001  dominf  8004  axdc2lem  8007  axdc3lem  8009  numthcor  8054  axdclem2  8080  alephsucpw  8125  dominfac  8128  canthp1lem1  8207  gchac  8228  intwun  8290  wunex2  8293  eltsk2g  8306  inttsk  8329  tskcard  8336  intgru  8369  gruina  8373  axgroth6  8383  npex  8543  axcnex  8702  pnfxr  10387  mnfxr  10388  ixxex  10598  prdsval  13282  prdsds  13290  prdshom  13293  ismre  13419  fnmre  13420  fnmrc  13436  mrcfval  13437  mrisval  13459  mreacs  13487  wunfunc  13700  catcfuccl  13868  catcxpccl  13908  lubfval  14039  glbfval  14044  isacs5lem  14199  issubm  14352  issubg  14548  cntzfval  14723  sylow1lem2  14837  lsmfval  14876  pj1fval  14930  issubrg  15472  lssset  15618  lspfval  15657  islbs  15756  lbsext  15843  lbsexg  15844  sraval  15856  aspval  15995  ocvfval  16493  cssval  16509  isobs  16547  istopon  16590  tgdom  16643  fncld  16686  leordtval2  16869  cnpfval  16891  iscnp2  16896  kgenf  17163  xkoopn  17211  xkouni  17221  dfac14  17239  xkoccn  17240  prdstopn  17249  xkoco1cn  17278  xkoco2cn  17279  xkococn  17281  xkoinjcn  17308  isfbas  17451  uzrest  17519  acufl  17539  alexsubALTlem2  17669  tsmsval2  17739  ishtpy  18397  vitali  18895  sspval  21224  shex  21716  hsupval  21838  ballotlemoex  22970  kur14lem9  23082  idlvalNEW  24777  intvlset  25030  issubcat  25177  vtarsuelt  25227  isconcl1b  25429  heibor1lem  25865  heibor  25877  idlval  25970  mzpclval  26135  eldiophb  26168  rpnnen3  26457  dfac11  26492  islinds  26611  rgspnval  26705  pmtrfval  26725  psubspset  29063  paddfval  29116  pclfvalN  29208  polfvalN  29223  psubclsetN  29255  docafvalN  30442  djafvalN  30454  dicval  30496  dochfval  30670  djhfval  30717  islpolN  30803
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-pow 4126
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-v 2742  df-in 3101  df-ss 3108  df-pw 3568
  Copyright terms: Public domain W3C validator