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

Theorem pwex 4165
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 3602 . . 3  |-  ( z  =  A  ->  ~P z  =  ~P A
)
32eleq1d 2324 . 2  |-  ( z  =  A  ->  ( ~P z  e.  _V  <->  ~P A  e.  _V )
)
4 df-pw 3601 . . 3  |-  ~P z  =  { y  |  y 
C_  z }
5 axpow2 4162 . . . . . 6  |-  E. x A. y ( y  C_  z  ->  y  e.  x
)
65bm1.3ii 4118 . . . . 5  |-  E. x A. y ( y  e.  x  <->  y  C_  z
)
7 abeq2 2363 . . . . . 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 2770 . . 3  |-  { y  |  y  C_  z }  e.  _V
114, 10eqeltri 2328 . 2  |-  ~P z  e.  _V
121, 3, 11vtocl 2813 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 2244   _Vcvv 2763    C_ wss 3127   ~Pcpw 3599
This theorem is referenced by:  pwexg  4166  p0ex  4169  pp0ex  4171  ord3ex  4172  abexssex  5715  fnpm  6748  canth2  6982  dffi3  7152  inf3lem7  7303  r1sucg  7409  r1pwOLD  7486  rankuni  7503  rankc2  7511  rankxpu  7516  rankxplim  7517  r0weon  7608  aceq3lem  7715  dfac5lem4  7721  dfac2a  7724  dfac2  7725  dfac8  7729  dfac13  7736  ackbij1lem5  7818  ackbij1lem8  7821  ackbij2lem2  7834  ackbij2lem3  7835  fin23lem17  7932  domtriomlem  8036  dominf  8039  axdc2lem  8042  axdc3lem  8044  numthcor  8089  axdclem2  8115  alephsucpw  8160  dominfac  8163  canthp1lem1  8242  gchac  8263  intwun  8325  wunex2  8328  eltsk2g  8341  inttsk  8364  tskcard  8371  intgru  8404  gruina  8408  axgroth6  8418  npex  8578  axcnex  8737  pnfxr  10422  mnfxr  10423  ixxex  10633  prdsval  13317  prdsds  13325  prdshom  13328  ismre  13454  fnmre  13455  fnmrc  13471  mrcfval  13472  mrisval  13494  mreacs  13522  wunfunc  13735  catcfuccl  13903  catcxpccl  13943  lubfval  14074  glbfval  14079  isacs5lem  14234  issubm  14387  issubg  14583  cntzfval  14758  sylow1lem2  14872  lsmfval  14911  pj1fval  14965  issubrg  15507  lssset  15653  lspfval  15692  islbs  15791  lbsext  15878  lbsexg  15879  sraval  15891  aspval  16030  ocvfval  16528  cssval  16544  isobs  16582  istopon  16625  tgdom  16678  fncld  16721  leordtval2  16904  cnpfval  16926  iscnp2  16931  kgenf  17198  xkoopn  17246  xkouni  17256  dfac14  17274  xkoccn  17275  prdstopn  17284  xkoco1cn  17313  xkoco2cn  17314  xkococn  17316  xkoinjcn  17343  isfbas  17486  uzrest  17554  acufl  17574  alexsubALTlem2  17704  tsmsval2  17774  ishtpy  18432  vitali  18930  sspval  21259  shex  21751  hsupval  21873  ballotlemoex  23005  kur14lem9  23117  idlvalNEW  24812  intvlset  25065  issubcat  25212  vtarsuelt  25262  isconcl1b  25464  heibor1lem  25900  heibor  25912  idlval  26005  mzpclval  26170  eldiophb  26203  rpnnen3  26492  dfac11  26527  islinds  26646  rgspnval  26740  pmtrfval  26760  psubspset  29100  paddfval  29153  pclfvalN  29245  polfvalN  29260  psubclsetN  29292  docafvalN  30479  djafvalN  30491  dicval  30533  dochfval  30707  djhfval  30754  islpolN  30840
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 2239  ax-sep 4115  ax-pow 4160
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 2245  df-cleq 2251  df-clel 2254  df-v 2765  df-in 3134  df-ss 3141  df-pw 3601
  Copyright terms: Public domain W3C validator