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

Theorem pwex 4192
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 3629 . . 3  |-  ( z  =  A  ->  ~P z  =  ~P A
)
32eleq1d 2350 . 2  |-  ( z  =  A  ->  ( ~P z  e.  _V  <->  ~P A  e.  _V )
)
4 df-pw 3628 . . 3  |-  ~P z  =  { y  |  y 
C_  z }
5 axpow2 4189 . . . . . 6  |-  E. x A. y ( y  C_  z  ->  y  e.  x
)
65bm1.3ii 4145 . . . . 5  |-  E. x A. y ( y  e.  x  <->  y  C_  z
)
7 abeq2 2389 . . . . . 6  |-  ( x  =  { y  |  y  C_  z }  <->  A. y ( y  e.  x  <->  y  C_  z
) )
87exbii 1574 . . . . 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 2796 . . 3  |-  { y  |  y  C_  z }  e.  _V
114, 10eqeltri 2354 . 2  |-  ~P z  e.  _V
121, 3, 11vtocl 2839 1  |-  ~P A  e.  _V
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1532   E.wex 1533    = wceq 1628    e. wcel 1688   {cab 2270   _Vcvv 2789    C_ wss 3153   ~Pcpw 3626
This theorem is referenced by:  pwexg  4193  p0ex  4196  pp0ex  4198  ord3ex  4199  abexssex  5742  fnpm  6775  canth2  7009  dffi3  7179  inf3lem7  7330  r1sucg  7436  r1pwOLD  7513  rankuni  7530  rankc2  7538  rankxpu  7543  rankxplim  7544  r0weon  7635  aceq3lem  7742  dfac5lem4  7748  dfac2a  7751  dfac2  7752  dfac8  7756  dfac13  7763  ackbij1lem5  7845  ackbij1lem8  7848  ackbij2lem2  7861  ackbij2lem3  7862  fin23lem17  7959  domtriomlem  8063  dominf  8066  axdc2lem  8069  axdc3lem  8071  numthcor  8116  axdclem2  8142  alephsucpw  8187  dominfac  8190  canthp1lem1  8269  gchac  8290  intwun  8352  wunex2  8355  eltsk2g  8368  inttsk  8391  tskcard  8398  intgru  8431  gruina  8435  axgroth6  8445  npex  8605  axcnex  8764  pnfxr  10450  mnfxr  10451  ixxex  10661  prdsval  13349  prdsds  13357  prdshom  13360  ismre  13486  fnmre  13487  fnmrc  13503  mrcfval  13504  mrisval  13526  mreacs  13554  wunfunc  13767  catcfuccl  13935  catcxpccl  13975  lubfval  14106  glbfval  14111  isacs5lem  14266  issubm  14419  issubg  14615  cntzfval  14790  sylow1lem2  14904  lsmfval  14943  pj1fval  14997  issubrg  15539  lssset  15685  lspfval  15724  islbs  15823  lbsext  15910  lbsexg  15911  sraval  15923  aspval  16062  ocvfval  16560  cssval  16576  isobs  16614  istopon  16657  tgdom  16710  fncld  16753  leordtval2  16936  cnpfval  16958  iscnp2  16963  kgenf  17230  xkoopn  17278  xkouni  17288  dfac14  17306  xkoccn  17307  prdstopn  17316  xkoco1cn  17345  xkoco2cn  17346  xkococn  17348  xkoinjcn  17375  isfbas  17518  uzrest  17586  acufl  17606  alexsubALTlem2  17736  tsmsval2  17806  ishtpy  18464  vitali  18962  sspval  21291  shex  21783  hsupval  21905  ballotlemoex  23037  kur14lem9  23149  idlvalNEW  24844  intvlset  25097  issubcat  25244  vtarsuelt  25294  isconcl1b  25496  heibor1lem  25932  heibor  25944  idlval  26037  mzpclval  26202  eldiophb  26235  rpnnen3  26524  dfac11  26559  islinds  26678  rgspnval  26772  pmtrfval  26792  psubspset  29200  paddfval  29253  pclfvalN  29345  polfvalN  29360  psubclsetN  29392  docafvalN  30579  djafvalN  30591  dicval  30633  dochfval  30807  djhfval  30854  islpolN  30940
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-14 1692  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265  ax-sep 4142  ax-pow 4187
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-v 2791  df-in 3160  df-ss 3167  df-pw 3628
  Copyright terms: Public domain W3C validator