Theorem pweqd 4015

Description: Equality deduction for power class. (Contributed by NM, 27-Nov-2013.)

Hypothesis

Ref	Expression
pweqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
pweqd	|- ( ph -> ~P A = ~P B )

Proof of Theorem pweqd

Step	Hyp	Ref	Expression
1		pweqd.1	. 2 |- ( ph -> A = B )
2		pweq 4013	. 2 |- ( A = B -> ~P A = ~P B )
3	1, 2	syl 16	1 |- ( ph -> ~P A = ~P B )

Syntax hints:   -> wi 4   = wceq 1379   ~Pcpw 4010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-pw 4012

This theorem is referenced by:  undefval  7005  pmvalg  7431  marypha1lem  7893  marypha1  7894  r1val3  8256  ackbij1lem5  8604  ackbij2lem2  8620  ackbij2lem3  8621  r1om  8624  isfin2  8674  hsmexlem8  8804  vdwmc  14355  hashbcval  14379  ismre  14845  mrcfval  14863  mrisval  14885  mreexexlemd  14899  brssc  15044  lubfval  15465  glbfval  15478  isclat  15596  issubm  15797  issubg  16006  cntzfval  16163  symgval  16209  lsmfval  16464  lsmpropd  16501  pj1fval  16518  issubrg  17229  lssset  17380  lspfval  17419  lsppropd  17464  islbs  17522  sraval  17622  aspval  17776  opsrval  17938  ply1frcl  18154  evls1fval  18155  ocvfval  18492  isobs  18546  islinds  18639  basis1  19246  baspartn  19250  cldval  19318  ntrfval  19319  clsfval  19320  mretopd  19387  neifval  19394  lpfval  19433  cncls2  19568  iscnrm  19618  iscnrm2  19633  2ndcsep  19754  kgenval  19799  xkoval  19851  dfac14  19882  qtopval  19959  qtopval2  19960  isfbas  20093  trfbas2  20107  flimval  20227  elflim  20235  flimclslem  20248  fclsfnflim  20291  fclscmp  20294  tsmsfbas  20389  tsmsval2  20391  ustval  20468  utopval  20498  mopnfss  20709  setsmstopn  20744  met2ndc  20789  istrkgb  23608  isumgra  24019  isuslgra  24047  isusgra  24048  edgss  24056  ismeas  27838  omsval  27932  oms0  27934  omsmon  27935  erdszelem3  28305  erdsze  28314  kur14  28328  iscvm  28372  heibor  29948  idlval  30041  igenval  30089  mzpclval  30289  dfac21  30644  islmodfg  30647  islssfg  30648  rgspnval  30750  isuhgr  31861  isushgr  31862  uhgun  31875  lincop  32108  lcoop  32111  islininds  32146  ldepsnlinc  32208  paddfval  34611  pclfvalN  34703  polfvalN  34718  docaffvalN  35936  docafvalN  35937  djaffvalN  35948  djafvalN  35949  dochffval  36164  dochfval  36165  djhffval  36211  djhfval  36212  lpolsetN  36297  lcdlss2N  36435