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

Theorem pwex 4209
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 3641 . . 3  |-  ( z  =  A  ->  ~P z  =  ~P A
)
32eleq1d 2362 . 2  |-  ( z  =  A  ->  ( ~P z  e.  _V  <->  ~P A  e.  _V )
)
4 df-pw 3640 . . 3  |-  ~P z  =  { y  |  y 
C_  z }
5 axpow2 4206 . . . . . 6  |-  E. x A. y ( y  C_  z  ->  y  e.  x
)
65bm1.3ii 4160 . . . . 5  |-  E. x A. y ( y  e.  x  <->  y  C_  z
)
7 abeq2 2401 . . . . . 6  |-  ( x  =  { y  |  y  C_  z }  <->  A. y ( y  e.  x  <->  y  C_  z
) )
87exbii 1572 . . . . 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 2808 . . 3  |-  { y  |  y  C_  z }  e.  _V
114, 10eqeltri 2366 . 2  |-  ~P z  e.  _V
121, 3, 11vtocl 2851 1  |-  ~P A  e.  _V
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1530   E.wex 1531    = wceq 1632    e. wcel 1696   {cab 2282   _Vcvv 2801    C_ wss 3165   ~Pcpw 3638
This theorem is referenced by:  pwexg  4210  p0ex  4213  pp0ex  4215  ord3ex  4216  abexssex  5797  fnpm  6796  canth2  7030  dffi3  7200  inf3lem7  7351  r1sucg  7457  r1pwOLD  7534  rankuni  7551  rankc2  7559  rankxpu  7564  rankxplim  7565  r0weon  7656  aceq3lem  7763  dfac5lem4  7769  dfac2a  7772  dfac2  7773  dfac8  7777  dfac13  7784  ackbij1lem5  7866  ackbij1lem8  7869  ackbij2lem2  7882  ackbij2lem3  7883  fin23lem17  7980  domtriomlem  8084  dominf  8087  axdc2lem  8090  axdc3lem  8092  numthcor  8137  axdclem2  8163  alephsucpw  8208  dominfac  8211  canthp1lem1  8290  gchac  8311  intwun  8373  wunex2  8376  eltsk2g  8389  inttsk  8412  tskcard  8419  intgru  8452  gruina  8456  axgroth6  8466  npex  8626  axcnex  8785  pnfxr  10471  mnfxr  10472  ixxex  10683  prdsval  13371  prdsds  13379  prdshom  13382  ismre  13508  fnmre  13509  fnmrc  13525  mrcfval  13526  mrisval  13548  mreacs  13576  wunfunc  13789  catcfuccl  13957  catcxpccl  13997  lubfval  14128  glbfval  14133  isacs5lem  14288  issubm  14441  issubg  14637  cntzfval  14812  sylow1lem2  14926  lsmfval  14965  pj1fval  15019  issubrg  15561  lssset  15707  lspfval  15746  islbs  15845  lbsext  15932  lbsexg  15933  sraval  15945  aspval  16084  ocvfval  16582  cssval  16598  isobs  16636  istopon  16679  tgdom  16732  fncld  16775  leordtval2  16958  cnpfval  16980  iscnp2  16985  kgenf  17252  xkoopn  17300  xkouni  17310  dfac14  17328  xkoccn  17329  prdstopn  17338  xkoco1cn  17367  xkoco2cn  17368  xkococn  17370  xkoinjcn  17397  isfbas  17540  uzrest  17608  acufl  17628  alexsubALTlem2  17758  tsmsval2  17828  ishtpy  18486  vitali  18984  sspval  21315  shex  21807  hsupval  21929  ballotlemoex  23060  isrnsigaOLD  23488  dmvlsiga  23505  coinflippv  23699  kur14lem9  23760  idlvalNEW  25548  intvlset  25801  issubcat  25948  vtarsuelt  25998  isconcl1b  26200  heibor1lem  26636  heibor  26648  idlval  26741  mzpclval  26906  eldiophb  26939  rpnnen3  27228  dfac11  27263  islinds  27382  rgspnval  27476  pmtrfval  27496  psubspset  30555  paddfval  30608  pclfvalN  30700  polfvalN  30715  psubclsetN  30747  docafvalN  31934  djafvalN  31946  dicval  31988  dochfval  32162  djhfval  32209  islpolN  32295
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-pow 4204
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-v 2803  df-in 3172  df-ss 3179  df-pw 3640
  Copyright terms: Public domain W3C validator