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

Theorem pweqd 3630
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 3628 . 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 1623   ~Pcpw 3625
This theorem is referenced by:  undefval  6301  pmvalg  6783  marypha1lem  7186  marypha1  7187  r1val3  7510  ackbij1lem5  7850  ackbij2lem2  7866  ackbij2lem3  7867  r1om  7870  isfin2  7920  hsmexlem8  8050  vdwmc  13025  hashbcval  13049  ismre  13492  mrcfval  13510  mrisval  13532  mreexexlemd  13546  brssc  13691  lubfval  14112  glbfval  14117  issubm  14425  issubg  14621  symgval  14771  cntzfval  14796  lsmfval  14949  lsmpropd  14986  pj1fval  15003  issubrg  15545  lssset  15691  lspfval  15730  lsppropd  15775  islbs  15829  sraval  15929  aspval  16068  opsrval  16216  ocvfval  16566  isobs  16620  basis1  16688  baspartn  16692  cldval  16760  ntrfval  16761  clsfval  16762  mretopd  16829  neifval  16836  lpfval  16870  cncls2  17002  iscnrm  17051  iscnrm2  17066  2ndcsep  17185  kgenval  17230  xkoval  17282  dfac14  17312  qtopval  17386  qtopval2  17387  isfbas  17524  trfbas2  17538  flimval  17658  elflim  17666  flimclslem  17679  fclsfnflim  17722  fclscmp  17725  tsmsfbas  17810  tsmsval2  17812  mopnfss  17989  setsmstopn  18024  met2ndc  18069  ismeas  23530  erdszelem3  23724  erdsze  23733  kur14  23747  iscvm  23790  isumgra  23867  iscst1  25174  prsubrtr  25399  idlvalNEW  25445  islimrs  25580  issubcat  25845  indcls2  25996  pfsubkl  26047  isconcl1b  26097  heibor  26545  idlval  26638  igenval  26686  mzpclval  26803  dfac21  27164  islmodfg  27167  islssfg  27168  islinds  27279  rgspnval  27373  isuslgra  28102  isusgra  28103  paddfval  29986  pclfvalN  30078  polfvalN  30093  docaffvalN  31311  docafvalN  31312  djaffvalN  31323  djafvalN  31324  dochffval  31539  dochfval  31540  djhffval  31586  djhfval  31587  lpolsetN  31672  lcdlss2N  31810
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-pw 3627
  Copyright terms: Public domain W3C validator