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

Theorem pweqd 4140
Description: Equality deduction for power class. (Contributed by NM, 27-Nov-2013.)
Hypothesis
Ref Expression
pweqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
pweqd (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)

Proof of Theorem pweqd
StepHypRef Expression
1 pweqd.1 . 2 (𝜑𝐴 = 𝐵)
2 pweq 4138 . 2 (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
31, 2syl 17 1 (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  𝒫 cpw 4135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3566  df-ss 3573  df-pw 4137
This theorem is referenced by:  undefval  7354  pmvalg  7820  marypha1lem  8291  marypha1  8292  r1val3  8653  ackbij1lem5  8998  ackbij2lem2  9014  ackbij2lem3  9015  r1om  9018  isfin2  9068  hsmexlem8  9198  vdwmc  15617  hashbcval  15641  ismre  16182  mrcfval  16200  mrisval  16222  mreexexlemd  16236  brssc  16406  lubfval  16910  glbfval  16923  isclat  17041  issubm  17279  issubg  17526  cntzfval  17685  symgval  17731  lsmfval  17985  lsmpropd  18022  pj1fval  18039  issubrg  18712  lssset  18866  lspfval  18905  lsppropd  18950  islbs  19008  sraval  19108  aspval  19260  opsrval  19406  ply1frcl  19615  evls1fval  19616  ocvfval  19942  isobs  19996  islinds  20080  basis1  20678  baspartn  20682  cldval  20750  ntrfval  20751  clsfval  20752  mretopd  20819  neifval  20826  lpfval  20865  cncls2  21000  iscnrm  21050  iscnrm2  21065  2ndcsep  21185  kgenval  21261  xkoval  21313  dfac14  21344  qtopval  21421  qtopval2  21422  isfbas  21556  trfbas2  21570  flimval  21690  elflim  21698  flimclslem  21711  fclsfnflim  21754  fclscmp  21757  tsmsfbas  21854  tsmsval2  21856  ustval  21929  utopval  21959  mopnfss  22171  setsmstopn  22206  met2ndc  22251  istrkgb  25271  isuhgr  25868  isushgr  25869  isuhgrop  25878  uhgrun  25882  uhgrstrrepe  25886  isupgr  25892  isumgr  25902  upgrun  25925  umgrun  25927  isuspgr  25957  isusgr  25958  isuspgrop  25966  isusgrop  25967  ausgrusgrb  25970  usgrstrrepe  26037  issubgr  26073  uhgrspansubgrlem  26092  usgrexi  26241  1hevtxdg1  26305  umgr2v2e  26324  ismeas  30067  omsval  30160  omscl  30162  omsf  30163  oms0  30164  carsgval  30170  omsmeas  30190  erdszelem3  30918  erdsze  30927  kur14  30941  iscvm  30984  mpstval  31175  mclsval  31203  heibor  33287  idlval  33479  igenval  33527  paddfval  34598  pclfvalN  34690  polfvalN  34705  docaffvalN  35925  docafvalN  35926  djaffvalN  35937  djafvalN  35938  dochffval  36153  dochfval  36154  djhffval  36200  djhfval  36201  lpolsetN  36286  lcdlss2N  36424  mzpclval  36803  dfac21  37151  islmodfg  37154  islssfg  37155  rgspnval  37254  rfovd  37812  fsovrfovd  37820  gneispace2  37947  sge0val  39916  ismea  40001  psmeasure  40021  caragenval  40040  isome  40041  omeunile  40052  isomennd  40078  ovnval  40088  hspmbl  40176  isvonmbl  40185  issubmgm  41103  lincop  41511  lcoop  41514  islininds  41549  ldepsnlinc  41611
  Copyright terms: Public domain W3C validator