Theorem pweqd 3967

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

Syntax hints:   -> wi 4   = wceq 1454   ~Pcpw 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3422  df-ss 3429  df-pw 3964

This theorem is referenced by:  undefval  7048  pmvalg  7508  marypha1lem  7972  marypha1  7973  r1val3  8334  ackbij1lem5  8679  ackbij2lem2  8695  ackbij2lem3  8696  r1om  8699  isfin2  8749  hsmexlem8  8879  vdwmc  14976  hashbcval  15002  ismre  15544  mrcfval  15562  mrisval  15584  mreexexlemd  15598  brssc  15767  lubfval  16272  glbfval  16285  isclat  16403  issubm  16642  issubg  16865  cntzfval  17022  symgval  17068  lsmfval  17338  lsmpropd  17375  pj1fval  17392  issubrg  18056  lssset  18205  lspfval  18244  lsppropd  18289  islbs  18347  sraval  18447  aspval  18600  opsrval  18746  ply1frcl  18955  evls1fval  18956  ocvfval  19277  isobs  19331  islinds  19415  basis1  20013  baspartn  20017  cldval  20086  ntrfval  20087  clsfval  20088  mretopd  20156  neifval  20163  lpfval  20202  cncls2  20337  iscnrm  20387  iscnrm2  20402  2ndcsep  20522  kgenval  20598  xkoval  20650  dfac14  20681  qtopval  20758  qtopval2  20759  isfbas  20892  trfbas2  20906  flimval  21026  elflim  21034  flimclslem  21047  fclsfnflim  21090  fclscmp  21093  tsmsfbas  21190  tsmsval2  21192  ustval  21265  utopval  21295  mopnfss  21506  setsmstopn  21541  met2ndc  21586  istrkgb  24551  isumgra  25090  isuslgra  25118  isusgra  25119  edgss  25127  ismeas  29069  omsval  29165  omscl  29167  omsf  29168  omsvalOLD  29169  omsclOLD  29171  omsfOLD  29172  oms0  29173  oms0OLD  29177  carsgval  29183  omsmeas  29203  omsmeasOLD  29204  erdszelem3  29964  erdsze  29973  kur14  29987  iscvm  30030  mpstval  30221  mclsval  30249  heibor  32197  idlval  32290  igenval  32338  paddfval  33406  pclfvalN  33498  polfvalN  33513  docaffvalN  34733  docafvalN  34734  djaffvalN  34745  djafvalN  34746  dochffval  34961  dochfval  34962  djhffval  35008  djhfval  35009  lpolsetN  35094  lcdlss2N  35232  mzpclval  35611  dfac21  35968  islmodfg  35971  islssfg  35972  rgspnval  36078  sge0val  38245  ismea  38326  psmeasure  38346  caragenval  38351  isome  38352  omeunile  38363  isomennd  38389  ovnval  38399  hspmbl  38488  isuhgr  39196  isushgr  39197  isuhgrop  39209  uhgrun  39213  isupgr  39222  isumgr  39231  upgrun  39253  umgrun  39255  isuspgr  39286  isusgr  39287  isusgrop  39296  ausgrusgrb  39299  issubgr  39392  uhgrspansubgrlem  39411  usgrexi  39555  umgr2v2e  39611  isuhgrALTV  39950  isushgrALTV  39951  uhgun  39964  issubmgm  40061  lincop  40473  lcoop  40476  islininds  40511  ldepsnlinc  40573