Theorem pweqd 3870

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 3868	. 2 |- ( A = B -> ~P A = ~P B )
3	1, 2	syl 16	1 |- ( ph -> ~P A = ~P B )

Syntax hints:   -> wi 4   = wceq 1369   ~Pcpw 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3340  df-ss 3347  df-pw 3867

This theorem is referenced by:  undefval  6800  pmvalg  7230  marypha1lem  7688  marypha1  7689  r1val3  8050  ackbij1lem5  8398  ackbij2lem2  8414  ackbij2lem3  8415  r1om  8418  isfin2  8468  hsmexlem8  8598  vdwmc  14044  hashbcval  14068  ismre  14533  mrcfval  14551  mrisval  14573  mreexexlemd  14587  brssc  14732  lubfval  15153  glbfval  15166  isclat  15284  issubm  15480  issubg  15686  cntzfval  15843  symgval  15889  lsmfval  16142  lsmpropd  16179  pj1fval  16196  issubrg  16870  lssset  17020  lspfval  17059  lsppropd  17104  islbs  17162  sraval  17262  aspval  17404  opsrval  17561  ply1frcl  17758  evls1fval  17759  ocvfval  18096  isobs  18150  islinds  18243  basis1  18560  baspartn  18564  cldval  18632  ntrfval  18633  clsfval  18634  mretopd  18701  neifval  18708  lpfval  18747  cncls2  18882  iscnrm  18932  iscnrm2  18947  2ndcsep  19068  kgenval  19113  xkoval  19165  dfac14  19196  qtopval  19273  qtopval2  19274  isfbas  19407  trfbas2  19421  flimval  19541  elflim  19549  flimclslem  19562  fclsfnflim  19605  fclscmp  19608  tsmsfbas  19703  tsmsval2  19705  ustval  19782  utopval  19812  mopnfss  20023  setsmstopn  20058  met2ndc  20103  istrkgb  22923  isumgra  23254  isuslgra  23276  isusgra  23277  ismeas  26618  omsval  26713  oms0  26715  omsmon  26716  erdszelem3  27086  erdsze  27095  kur14  27109  iscvm  27153  heibor  28725  idlval  28818  igenval  28866  mzpclval  29066  dfac21  29424  islmodfg  29427  islssfg  29428  rgspnval  29530  lincop  30947  lcoop  30950  islininds  30985  ldepsnlinc  31055  paddfval  33446  pclfvalN  33538  polfvalN  33553  docaffvalN  34771  docafvalN  34772  djaffvalN  34783  djafvalN  34784  dochffval  34999  dochfval  35000  djhffval  35046  djhfval  35047  lpolsetN  35132  lcdlss2N  35270