MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pweqd Unicode version

Theorem pweqd 3719
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
StepHypRef Expression
1 pweqd.1 . 2  |-  ( ph  ->  A  =  B )
2 pweq 3717 . 2  |-  ( A  =  B  ->  ~P A  =  ~P B
)
31, 2syl 15 1  |-  ( ph  ->  ~P A  =  ~P B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647   ~Pcpw 3714
This theorem is referenced by:  undefval  6443  pmvalg  6926  marypha1lem  7333  marypha1  7334  r1val3  7657  ackbij1lem5  7997  ackbij2lem2  8013  ackbij2lem3  8014  r1om  8017  isfin2  8067  hsmexlem8  8197  vdwmc  13233  hashbcval  13257  ismre  13702  mrcfval  13720  mrisval  13742  mreexexlemd  13756  brssc  13901  lubfval  14322  glbfval  14327  issubm  14635  issubg  14831  symgval  14981  cntzfval  15006  lsmfval  15159  lsmpropd  15196  pj1fval  15213  issubrg  15755  lssset  15901  lspfval  15940  lsppropd  15985  islbs  16039  sraval  16139  aspval  16278  opsrval  16426  ocvfval  16783  isobs  16837  basis1  16905  baspartn  16909  cldval  16977  ntrfval  16978  clsfval  16979  mretopd  17046  neifval  17053  lpfval  17087  cncls2  17219  iscnrm  17268  iscnrm2  17283  2ndcsep  17402  kgenval  17447  xkoval  17499  dfac14  17529  qtopval  17603  qtopval2  17604  isfbas  17737  trfbas2  17751  flimval  17871  elflim  17879  flimclslem  17892  fclsfnflim  17935  fclscmp  17938  tsmsfbas  18023  tsmsval2  18025  mopnfss  18202  setsmstopn  18237  met2ndc  18282  isumgra  21028  isuslgra  21050  isusgra  21051  ustval  23707  utopval  23735  ismeas  24018  erdszelem3  24327  erdsze  24336  kur14  24350  iscvm  24393  heibor  26051  idlval  26144  igenval  26192  mzpclval  26309  dfac21  26670  islmodfg  26673  islssfg  26674  islinds  26785  rgspnval  26879  paddfval  30057  pclfvalN  30149  polfvalN  30164  docaffvalN  31382  docafvalN  31383  djaffvalN  31394  djafvalN  31395  dochffval  31610  dochfval  31611  djhffval  31657  djhfval  31658  lpolsetN  31743  lcdlss2N  31881
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-in 3245  df-ss 3252  df-pw 3716
  Copyright terms: Public domain W3C validator