MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwex Structured version   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  5994  fnpm  7018  canth2  7252  dffi3  7428  inf3lem7  7581  r1sucg  7687  r1pwOLD  7764  rankuni  7781  rankc2  7789  rankxpu  7794  rankxplim  7795  r0weon  7886  aceq3lem  7993  dfac5lem4  7999  dfac2a  8002  dfac2  8003  dfac8  8007  dfac13  8014  ackbij1lem5  8096  ackbij1lem8  8099  ackbij2lem2  8112  ackbij2lem3  8113  fin23lem17  8210  domtriomlem  8314  dominf  8317  axdc2lem  8320  axdc3lem  8322  numthcor  8366  axdclem2  8392  alephsucpw  8437  dominfac  8440  canthp1lem1  8519  gchac  8540  intwun  8602  wunex2  8605  eltsk2g  8618  inttsk  8641  tskcard  8648  intgru  8681  gruina  8685  axgroth6  8695  npex  8855  axcnex  9014  pnfxr  10705  mnfxr  10706  ixxex  10919  prdsval  13670  prdsds  13678  prdshom  13681  ismre  13807  fnmre  13808  fnmrc  13824  mrcfval  13825  mrisval  13847  mreacs  13875  wunfunc  14088  catcfuccl  14256  catcxpccl  14296  lubfval  14427  glbfval  14432  isacs5lem  14587  issubm  14740  issubg  14936  cntzfval  15111  sylow1lem2  15225  lsmfval  15264  pj1fval  15318  issubrg  15860  lssset  16002  lspfval  16041  islbs  16140  lbsext  16227  lbsexg  16228  sraval  16240  aspval  16379  ocvfval  16885  cssval  16901  isobs  16939  istopon  16982  tgdom  17035  fncld  17078  leordtval2  17268  cnpfval  17290  iscnp2  17295  kgenf  17565  xkoopn  17613  xkouni  17623  dfac14  17642  xkoccn  17643  prdstopn  17652  xkoco1cn  17681  xkoco2cn  17682  xkococn  17684  xkoinjcn  17711  isfbas  17853  uzrest  17921  acufl  17941  alexsubALTlem2  18071  tsmsval2  18151  ustfn  18223  ustn0  18242  ishtpy  18989  vitali  19497  sspval  22214  shex  22706  hsupval  22828  isrnsigaOLD  24487  dmvlsiga  24504  coinflippv  24733  ballotlemoex  24735  kur14lem9  24892  heibor1lem  26509  heibor  26521  idlval  26614  mzpclval  26773  eldiophb  26806  rpnnen3  27094  dfac11  27128  islinds  27247  rgspnval  27341  pmtrfval  27361  psubspset  30478  paddfval  30531  pclfvalN  30623  polfvalN  30638  psubclsetN  30670  docafvalN  31857  djafvalN  31869  dicval  31911  dochfval  32085  djhfval  32132  islpolN  32218
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