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

Theorem pwex 4374
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 3794 . . 3  |-  ( z  =  A  ->  ~P z  =  ~P A
)
32eleq1d 2501 . 2  |-  ( z  =  A  ->  ( ~P z  e.  _V  <->  ~P A  e.  _V )
)
4 df-pw 3793 . . 3  |-  ~P z  =  { y  |  y 
C_  z }
5 axpow2 4371 . . . . . 6  |-  E. x A. y ( y  C_  z  ->  y  e.  x
)
65bm1.3ii 4325 . . . . 5  |-  E. x A. y ( y  e.  x  <->  y  C_  z
)
7 abeq2 2540 . . . . . 6  |-  ( x  =  { y  |  y  C_  z }  <->  A. y ( y  e.  x  <->  y  C_  z
) )
87exbii 1592 . . . . 5  |-  ( E. x  x  =  {
y  |  y  C_  z }  <->  E. x A. y
( y  e.  x  <->  y 
C_  z ) )
96, 8mpbir 201 . . . 4  |-  E. x  x  =  { y  |  y  C_  z }
109issetri 2955 . . 3  |-  { y  |  y  C_  z }  e.  _V
114, 10eqeltri 2505 . 2  |-  ~P z  e.  _V
121, 3, 11vtocl 2998 1  |-  ~P A  e.  _V
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1549   E.wex 1550    = wceq 1652    e. wcel 1725   {cab 2421   _Vcvv 2948    C_ wss 3312   ~Pcpw 3791
This theorem is referenced by:  pwexg  4375  p0ex  4378  pp0ex  4380  ord3ex  4381  abexssex  5993  fnpm  7017  canth2  7251  dffi3  7427  inf3lem7  7578  r1sucg  7684  r1pwOLD  7761  rankuni  7778  rankc2  7786  rankxpu  7791  rankxplim  7792  r0weon  7883  aceq3lem  7990  dfac5lem4  7996  dfac2a  7999  dfac2  8000  dfac8  8004  dfac13  8011  ackbij1lem5  8093  ackbij1lem8  8096  ackbij2lem2  8109  ackbij2lem3  8110  fin23lem17  8207  domtriomlem  8311  dominf  8314  axdc2lem  8317  axdc3lem  8319  numthcor  8363  axdclem2  8389  alephsucpw  8434  dominfac  8437  canthp1lem1  8516  gchac  8537  intwun  8599  wunex2  8602  eltsk2g  8615  inttsk  8638  tskcard  8645  intgru  8678  gruina  8682  axgroth6  8692  npex  8852  axcnex  9011  pnfxr  10702  mnfxr  10703  ixxex  10916  prdsval  13666  prdsds  13674  prdshom  13677  ismre  13803  fnmre  13804  fnmrc  13820  mrcfval  13821  mrisval  13843  mreacs  13871  wunfunc  14084  catcfuccl  14252  catcxpccl  14292  lubfval  14423  glbfval  14428  isacs5lem  14583  issubm  14736  issubg  14932  cntzfval  15107  sylow1lem2  15221  lsmfval  15260  pj1fval  15314  issubrg  15856  lssset  15998  lspfval  16037  islbs  16136  lbsext  16223  lbsexg  16224  sraval  16236  aspval  16375  ocvfval  16881  cssval  16897  isobs  16935  istopon  16978  tgdom  17031  fncld  17074  leordtval2  17264  cnpfval  17286  iscnp2  17291  kgenf  17561  xkoopn  17609  xkouni  17619  dfac14  17638  xkoccn  17639  prdstopn  17648  xkoco1cn  17677  xkoco2cn  17678  xkococn  17680  xkoinjcn  17707  isfbas  17849  uzrest  17917  acufl  17937  alexsubALTlem2  18067  tsmsval2  18147  ustfn  18219  ustn0  18238  ishtpy  18985  vitali  19493  sspval  22210  shex  22702  hsupval  22824  isrnsigaOLD  24483  dmvlsiga  24500  coinflippv  24729  ballotlemoex  24731  kur14lem9  24888  heibor1lem  26455  heibor  26467  idlval  26560  mzpclval  26719  eldiophb  26752  rpnnen3  27040  dfac11  27075  islinds  27194  rgspnval  27288  pmtrfval  27308  psubspset  30380  paddfval  30433  pclfvalN  30525  polfvalN  30540  psubclsetN  30572  docafvalN  31759  djafvalN  31771  dicval  31813  dochfval  31987  djhfval  32034  islpolN  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-pow 4369
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-v 2950  df-in 3319  df-ss 3326  df-pw 3793
  Copyright terms: Public domain W3C validator