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

Theorem pwex 4385
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 3804 . . 3  |-  ( z  =  A  ->  ~P z  =  ~P A
)
32eleq1d 2504 . 2  |-  ( z  =  A  ->  ( ~P z  e.  _V  <->  ~P A  e.  _V )
)
4 df-pw 3803 . . 3  |-  ~P z  =  { y  |  y 
C_  z }
5 axpow2 4382 . . . . . 6  |-  E. x A. y ( y  C_  z  ->  y  e.  x
)
65bm1.3ii 4336 . . . . 5  |-  E. x A. y ( y  e.  x  <->  y  C_  z
)
7 abeq2 2543 . . . . . 6  |-  ( x  =  { y  |  y  C_  z }  <->  A. y ( y  e.  x  <->  y  C_  z
) )
87exbii 1593 . . . . 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 2965 . . 3  |-  { y  |  y  C_  z }  e.  _V
114, 10eqeltri 2508 . 2  |-  ~P z  e.  _V
121, 3, 11vtocl 3008 1  |-  ~P A  e.  _V
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1550   E.wex 1551    = wceq 1653    e. wcel 1726   {cab 2424   _Vcvv 2958    C_ wss 3322   ~Pcpw 3801
This theorem is referenced by:  pwexg  4386  p0ex  4389  pp0ex  4391  ord3ex  4392  abexssex  6005  fnpm  7029  canth2  7263  dffi3  7439  inf3lem7  7592  r1sucg  7698  r1pwOLD  7775  rankuni  7792  rankc2  7800  rankxpu  7805  rankmapu  7807  rankxplim  7808  r0weon  7899  aceq3lem  8006  dfac5lem4  8012  dfac2a  8015  dfac2  8016  dfac8  8020  dfac13  8027  ackbij1lem5  8109  ackbij1lem8  8112  ackbij2lem2  8125  ackbij2lem3  8126  fin23lem17  8223  domtriomlem  8327  dominf  8330  axdc2lem  8333  axdc3lem  8335  numthcor  8379  axdclem2  8405  alephsucpw  8450  dominfac  8453  canthp1lem1  8532  gchac  8561  intwun  8615  wunex2  8618  eltsk2g  8631  inttsk  8654  tskcard  8661  intgru  8694  gruina  8698  axgroth6  8708  npex  8868  axcnex  9027  pnfxr  10718  mnfxr  10719  ixxex  10932  prdsval  13683  prdsds  13691  prdshom  13694  ismre  13820  fnmre  13821  fnmrc  13837  mrcfval  13838  mrisval  13860  mreacs  13888  wunfunc  14101  catcfuccl  14269  catcxpccl  14309  lubfval  14440  glbfval  14445  isacs5lem  14600  issubm  14753  issubg  14949  cntzfval  15124  sylow1lem2  15238  lsmfval  15277  pj1fval  15331  issubrg  15873  lssset  16015  lspfval  16054  islbs  16153  lbsext  16240  lbsexg  16241  sraval  16253  aspval  16392  ocvfval  16898  cssval  16914  isobs  16952  istopon  16995  tgdom  17048  fncld  17091  leordtval2  17281  cnpfval  17303  iscnp2  17308  kgenf  17578  xkoopn  17626  xkouni  17636  dfac14  17655  xkoccn  17656  prdstopn  17665  xkoco1cn  17694  xkoco2cn  17695  xkococn  17697  xkoinjcn  17724  isfbas  17866  uzrest  17934  acufl  17954  alexsubALTlem2  18084  tsmsval2  18164  ustfn  18236  ustn0  18255  ishtpy  19002  vitali  19510  sspval  22227  shex  22719  hsupval  22841  isrnsigaOLD  24500  dmvlsiga  24517  coinflippv  24746  ballotlemoex  24748  kur14lem9  24905  heibor1lem  26532  heibor  26544  idlval  26637  mzpclval  26796  eldiophb  26829  rpnnen3  27117  dfac11  27151  islinds  27270  rgspnval  27364  pmtrfval  27384  psubspset  30615  paddfval  30668  pclfvalN  30760  polfvalN  30775  psubclsetN  30807  docafvalN  31994  djafvalN  32006  dicval  32048  dochfval  32222  djhfval  32269  islpolN  32355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-pow 4380
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-v 2960  df-in 3329  df-ss 3336  df-pw 3803
  Copyright terms: Public domain W3C validator