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

Theorem pweqd 3806
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 3804 . 2  |-  ( A  =  B  ->  ~P A  =  ~P B
)
31, 2syl 16 1  |-  ( ph  ->  ~P A  =  ~P B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   ~Pcpw 3801
This theorem is referenced by:  undefval  6548  pmvalg  7031  marypha1lem  7440  marypha1  7441  r1val3  7766  ackbij1lem5  8106  ackbij2lem2  8122  ackbij2lem3  8123  r1om  8126  isfin2  8176  hsmexlem8  8306  vdwmc  13348  hashbcval  13372  ismre  13817  mrcfval  13835  mrisval  13857  mreexexlemd  13871  brssc  14016  lubfval  14437  glbfval  14442  issubm  14750  issubg  14946  symgval  15096  cntzfval  15121  lsmfval  15274  lsmpropd  15311  pj1fval  15328  issubrg  15870  lssset  16012  lspfval  16051  lsppropd  16096  islbs  16150  sraval  16250  aspval  16389  opsrval  16537  ocvfval  16895  isobs  16949  basis1  17017  baspartn  17021  cldval  17089  ntrfval  17090  clsfval  17091  mretopd  17158  neifval  17165  lpfval  17204  cncls2  17339  iscnrm  17389  iscnrm2  17404  2ndcsep  17524  kgenval  17569  xkoval  17621  dfac14  17652  qtopval  17729  qtopval2  17730  isfbas  17863  trfbas2  17877  flimval  17997  elflim  18005  flimclslem  18018  fclsfnflim  18061  fclscmp  18064  tsmsfbas  18159  tsmsval2  18161  ustval  18234  utopval  18264  mopnfss  18475  setsmstopn  18510  met2ndc  18555  isumgra  21352  isuslgra  21374  isusgra  21375  ismeas  24555  erdszelem3  24881  erdsze  24890  kur14  24904  iscvm  24948  heibor  26532  idlval  26625  igenval  26673  mzpclval  26784  dfac21  27143  islmodfg  27146  islssfg  27147  islinds  27258  rgspnval  27352  paddfval  30656  pclfvalN  30748  polfvalN  30763  docaffvalN  31981  docafvalN  31982  djaffvalN  31993  djafvalN  31994  dochffval  32209  dochfval  32210  djhffval  32256  djhfval  32257  lpolsetN  32342  lcdlss2N  32480
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336  df-pw 3803
  Copyright terms: Public domain W3C validator