Theorem pweqd 4002

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

Syntax hints:   -> wi 4   = wceq 1383   ~Pcpw 3997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475  df-pw 3999

This theorem is referenced by:  undefval  7007  pmvalg  7433  marypha1lem  7895  marypha1  7896  r1val3  8259  ackbij1lem5  8607  ackbij2lem2  8623  ackbij2lem3  8624  r1om  8627  isfin2  8677  hsmexlem8  8807  vdwmc  14478  hashbcval  14502  ismre  14969  mrcfval  14987  mrisval  15009  mreexexlemd  15023  brssc  15165  lubfval  15587  glbfval  15600  isclat  15718  issubm  15957  issubg  16180  cntzfval  16337  symgval  16383  lsmfval  16637  lsmpropd  16674  pj1fval  16691  issubrg  17408  lssset  17559  lspfval  17598  lsppropd  17643  islbs  17701  sraval  17801  aspval  17956  opsrval  18118  ply1frcl  18334  evls1fval  18335  ocvfval  18675  isobs  18729  islinds  18822  basis1  19429  baspartn  19433  cldval  19502  ntrfval  19503  clsfval  19504  mretopd  19571  neifval  19578  lpfval  19617  cncls2  19752  iscnrm  19802  iscnrm2  19817  2ndcsep  19938  kgenval  20014  xkoval  20066  dfac14  20097  qtopval  20174  qtopval2  20175  isfbas  20308  trfbas2  20322  flimval  20442  elflim  20450  flimclslem  20463  fclsfnflim  20506  fclscmp  20509  tsmsfbas  20604  tsmsval2  20606  ustval  20683  utopval  20713  mopnfss  20924  setsmstopn  20959  met2ndc  21004  istrkgb  23830  isumgra  24293  isuslgra  24321  isusgra  24322  edgss  24330  ismeas  28148  omsval  28242  oms0  28244  omsmon  28245  erdszelem3  28615  erdsze  28624  kur14  28638  iscvm  28682  mpstval  28873  mclsval  28901  heibor  30293  idlval  30386  igenval  30434  mzpclval  30633  dfac21  30988  islmodfg  30991  islssfg  30992  rgspnval  31093  isuhgr  32320  isushgr  32321  uhgun  32334  issubmgm  32431  lincop  32879  lcoop  32882  islininds  32917  ldepsnlinc  32979  paddfval  35396  pclfvalN  35488  polfvalN  35503  docaffvalN  36723  docafvalN  36724  djaffvalN  36735  djafvalN  36736  dochffval  36951  dochfval  36952  djhffval  36998  djhfval  36999  lpolsetN  37084  lcdlss2N  37222