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

Theorem pwex 4087
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 3533 . . 3  |-  ( z  =  A  ->  ~P z  =  ~P A
)
32eleq1d 2319 . 2  |-  ( z  =  A  ->  ( ~P z  e.  _V  <->  ~P A  e.  _V )
)
4 df-pw 3532 . . 3  |-  ~P z  =  { y  |  y 
C_  z }
5 axpow2 4084 . . . . . 6  |-  E. x A. y ( y  C_  z  ->  y  e.  x
)
65bm1.3ii 4041 . . . . 5  |-  E. x A. y ( y  e.  x  <->  y  C_  z
)
7 abeq2 2354 . . . . . 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 2734 . . 3  |-  { y  |  y  C_  z }  e.  _V
114, 10eqeltri 2323 . 2  |-  ~P z  e.  _V
121, 3, 11vtocl 2776 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 2239   _Vcvv 2727    C_ wss 3078   ~Pcpw 3530
This theorem is referenced by:  pwexg  4088  p0ex  4091  pp0ex  4093  ord3ex  4094  abexssex  5633  fnpm  6666  canth2  6899  dffi3  7068  inf3lem7  7219  r1sucg  7325  r1pwOLD  7402  rankuni  7419  rankc2  7427  rankxpu  7432  rankxplim  7433  r0weon  7524  aceq3lem  7631  dfac5lem4  7637  dfac2a  7640  dfac2  7641  dfac8  7645  dfac13  7652  ackbij1lem5  7734  ackbij1lem8  7737  ackbij2lem2  7750  ackbij2lem3  7751  fin23lem17  7848  domtriomlem  7952  dominf  7955  axdc2lem  7958  axdc3lem  7960  numthcor  8005  axdclem2  8031  alephsucpw  8072  dominfac  8075  canthp1lem1  8154  gchac  8175  intwun  8237  wunex2  8240  eltsk2g  8253  inttsk  8276  tskcard  8283  intgru  8316  gruina  8320  axgroth6  8330  npex  8490  axcnex  8649  pnfxr  10334  mnfxr  10335  ixxex  10545  prdsval  13229  prdsds  13237  prdshom  13240  ismre  13364  fnmre  13365  fnmrc  13381  mrcfval  13382  mreacs  13404  wunfunc  13617  catcfuccl  13785  catcxpccl  13825  lubfval  13956  glbfval  13961  isacs5lem  14116  issubm  14260  issubg  14456  cntzfval  14631  sylow1lem2  14745  lsmfval  14784  pj1fval  14838  issubrg  15380  lssset  15526  lspfval  15565  islbs  15664  lbsext  15748  lbsexg  15749  sraval  15761  aspval  15900  ocvfval  16398  cssval  16414  isobs  16452  istopon  16495  tgdom  16548  fncld  16591  leordtval2  16774  cnpfval  16796  iscnp2  16801  kgenf  17068  xkoopn  17116  xkouni  17126  dfac14  17144  xkoccn  17145  prdstopn  17154  xkoco1cn  17183  xkoco2cn  17184  xkococn  17186  xkoinjcn  17213  isfbas  17356  uzrest  17424  acufl  17444  alexsubALTlem2  17574  tsmsval2  17644  ishtpy  18302  vitali  18800  sspval  21129  shex  21621  hsupval  21743  kur14lem9  22916  idlvalNEW  24611  intvlset  24864  issubcat  25011  vtarsuelt  25061  isconcl1b  25263  heibor1lem  25699  heibor  25711  idlval  25804  mzpclval  25969  eldiophb  26002  rpnnen3  26291  dfac11  26326  islinds  26445  rgspnval  26539  pmtrfval  26559  psubspset  28734  paddfval  28787  pclfvalN  28879  polfvalN  28894  psubclsetN  28926  docafvalN  30113  djafvalN  30125  dicval  30167  dochfval  30341  djhfval  30388  islpolN  30474
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 1926  ax-ext 2234  ax-sep 4038  ax-pow 4082
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-v 2729  df-in 3085  df-ss 3089  df-pw 3532
  Copyright terms: Public domain W3C validator