Theorem pweqd 4004

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

Syntax hints:   -> wi 4   = wceq 1398   ~Pcpw 3999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475  df-pw 4001

This theorem is referenced by:  undefval  6997  pmvalg  7423  marypha1lem  7885  marypha1  7886  r1val3  8247  ackbij1lem5  8595  ackbij2lem2  8611  ackbij2lem3  8612  r1om  8615  isfin2  8665  hsmexlem8  8795  vdwmc  14583  hashbcval  14607  ismre  15082  mrcfval  15100  mrisval  15122  mreexexlemd  15136  brssc  15305  lubfval  15810  glbfval  15823  isclat  15941  issubm  16180  issubg  16403  cntzfval  16560  symgval  16606  lsmfval  16860  lsmpropd  16897  pj1fval  16914  issubrg  17627  lssset  17778  lspfval  17817  lsppropd  17862  islbs  17920  sraval  18020  aspval  18175  opsrval  18337  ply1frcl  18553  evls1fval  18554  ocvfval  18873  isobs  18927  islinds  19014  basis1  19621  baspartn  19625  cldval  19694  ntrfval  19695  clsfval  19696  mretopd  19763  neifval  19770  lpfval  19809  cncls2  19944  iscnrm  19994  iscnrm2  20009  2ndcsep  20129  kgenval  20205  xkoval  20257  dfac14  20288  qtopval  20365  qtopval2  20366  isfbas  20499  trfbas2  20513  flimval  20633  elflim  20641  flimclslem  20654  fclsfnflim  20697  fclscmp  20700  tsmsfbas  20795  tsmsval2  20797  ustval  20874  utopval  20904  mopnfss  21115  setsmstopn  21150  met2ndc  21195  istrkgb  24053  isumgra  24520  isuslgra  24548  isusgra  24549  edgss  24557  ismeas  28410  omsval  28504  omscl  28506  omsf  28507  oms0  28508  carsgval  28514  omsmeas  28534  erdszelem3  28904  erdsze  28913  kur14  28927  iscvm  28971  mpstval  29162  mclsval  29190  heibor  30560  idlval  30653  igenval  30701  mzpclval  30900  dfac21  31254  islmodfg  31257  islssfg  31258  rgspnval  31361  isuhgr  32757  isushgr  32758  uhgun  32771  issubmgm  32868  lincop  33282  lcoop  33285  islininds  33320  ldepsnlinc  33382  paddfval  35937  pclfvalN  36029  polfvalN  36044  docaffvalN  37264  docafvalN  37265  djaffvalN  37276  djafvalN  37277  dochffval  37492  dochfval  37493  djhffval  37539  djhfval  37540  lpolsetN  37625  lcdlss2N  37763