Theorem pweqd 3984

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

Syntax hints:   -> wi 4   = wceq 1437   ~Pcpw 3979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450  df-pw 3981

This theorem is referenced by:  undefval  7028  pmvalg  7488  marypha1lem  7950  marypha1  7951  r1val3  8311  ackbij1lem5  8655  ackbij2lem2  8671  ackbij2lem3  8672  r1om  8675  isfin2  8725  hsmexlem8  8855  vdwmc  14916  hashbcval  14942  ismre  15484  mrcfval  15502  mrisval  15524  mreexexlemd  15538  brssc  15707  lubfval  16212  glbfval  16225  isclat  16343  issubm  16582  issubg  16805  cntzfval  16962  symgval  17008  lsmfval  17278  lsmpropd  17315  pj1fval  17332  issubrg  17996  lssset  18145  lspfval  18184  lsppropd  18229  islbs  18287  sraval  18387  aspval  18540  opsrval  18686  ply1frcl  18895  evls1fval  18896  ocvfval  19216  isobs  19270  islinds  19354  basis1  19952  baspartn  19956  cldval  20025  ntrfval  20026  clsfval  20027  mretopd  20095  neifval  20102  lpfval  20141  cncls2  20276  iscnrm  20326  iscnrm2  20341  2ndcsep  20461  kgenval  20537  xkoval  20589  dfac14  20620  qtopval  20697  qtopval2  20698  isfbas  20831  trfbas2  20845  flimval  20965  elflim  20973  flimclslem  20986  fclsfnflim  21029  fclscmp  21032  tsmsfbas  21129  tsmsval2  21131  ustval  21204  utopval  21234  mopnfss  21445  setsmstopn  21480  met2ndc  21525  istrkgb  24490  isumgra  25029  isuslgra  25057  isusgra  25058  edgss  25066  ismeas  29017  omsval  29113  omscl  29115  omsf  29116  omsvalOLD  29117  omsclOLD  29119  omsfOLD  29120  oms0  29121  oms0OLD  29125  carsgval  29131  omsmeas  29151  omsmeasOLD  29152  erdszelem3  29912  erdsze  29921  kur14  29935  iscvm  29978  mpstval  30169  mclsval  30197  heibor  32067  idlval  32160  igenval  32208  paddfval  33281  pclfvalN  33373  polfvalN  33388  docaffvalN  34608  docafvalN  34609  djaffvalN  34620  djafvalN  34621  dochffval  34836  dochfval  34837  djhffval  34883  djhfval  34884  lpolsetN  34969  lcdlss2N  35107  mzpclval  35486  dfac21  35844  islmodfg  35847  islssfg  35848  rgspnval  35954  sge0val  37996  ismea  38068  psmeasure  38088  caragenval  38093  isome  38094  omeunile  38105  isomennd  38131  ovnval  38137  isuhgr  38814  isushgr  38815  uhgrop  38825  uhgrres  38830  uhgrun  38833  isumgr  38837  umgrres  38846  umgrun  38856  isuslgr  38868  isusgr  38869  ausgrusgrb  38879  usgrres  38895  isuhgrALTV  38950  isushgrALTV  38951  uhgun  38964  issubmgm  39061  lincop  39475  lcoop  39478  islininds  39513  ldepsnlinc  39575