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

Theorem pweqd 4540
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 4538 . 2 (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
31, 2syl 17 1 (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  𝒫 cpw 4535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949  df-pw 4537
This theorem is referenced by:  undefval  7931  pmvalg  8406  marypha1lem  8885  marypha1  8886  r1val3  9255  ackbij2lem2  9650  ackbij2lem3  9651  r1om  9654  isfin2  9704  hsmexlem8  9834  vdwmc  16302  hashbcval  16326  ismre  16849  mrcfval  16867  mrisval  16889  mreexexlemd  16903  brssc  17072  lubfval  17576  glbfval  17589  isclat  17707  issubm  17956  issubg  18217  cntzfval  18388  symgval  18435  lsmfval  18692  lsmpropd  18732  pj1fval  18749  issubrg  19464  lssset  19634  lspfval  19674  lsppropd  19719  islbs  19777  sraval  19877  aspval  20030  opsrval  20183  ply1frcl  20409  evls1fval  20410  ocvfval  20738  isobs  20792  islinds  20881  basis1  21486  baspartn  21490  cldval  21559  ntrfval  21560  clsfval  21561  mretopd  21628  neifval  21635  lpfval  21674  cncls2  21809  iscnrm  21859  iscnrm2  21874  2ndcsep  21995  kgenval  22071  xkoval  22123  dfac14  22154  qtopval  22231  qtopval2  22232  isfbas  22365  trfbas2  22379  flimval  22499  elflim  22507  flimclslem  22520  fclsfnflim  22563  fclscmp  22566  tsmsfbas  22663  tsmsval2  22665  ustval  22738  utopval  22768  mopnfss  22980  setsmstopn  23015  met2ndc  23060  istrkgb  26168  isuhgr  26772  isushgr  26773  isuhgrop  26782  uhgrun  26786  uhgrstrrepe  26790  isupgr  26796  upgrop  26806  isumgr  26807  upgrun  26830  umgrun  26832  isuspgr  26864  isusgr  26865  isuspgrop  26873  isusgrop  26874  ausgrusgrb  26877  usgrstrrepe  26944  issubgr  26980  uhgrspansubgrlem  26999  usgrexi  27150  1hevtxdg1  27215  umgr2v2e  27234  ismeas  31357  omsval  31450  omscl  31452  omsf  31453  oms0  31454  carsgval  31460  omsmeas  31480  erdszelem3  32337  erdsze  32346  kur14  32360  iscvm  32403  mpstval  32679  mclsval  32707  madeval  33186  bj-imdirval  34364  pibp21  34578  heibor  34980  idlval  35172  igenval  35220  paddfval  36813  pclfvalN  36905  polfvalN  36920  docaffvalN  38137  docafvalN  38138  djaffvalN  38149  djafvalN  38150  dochffval  38365  dochfval  38366  djhffval  38412  djhfval  38413  lpolsetN  38498  lcdlss2N  38636  mzpclval  39200  dfac21  39544  islmodfg  39547  islssfg  39548  rgspnval  39646  rfovd  40225  fsovrfovd  40233  gneispace2  40360  ismnu  40474  sge0val  42525  ismea  42610  psmeasure  42630  caragenval  42652  isome  42653  omeunile  42664  isomennd  42690  ovnval  42700  hspmbl  42788  isvonmbl  42797  afv2eq12d  43291  issubmgm  43933  lincop  44391  lcoop  44394  islininds  44429  ldepsnlinc  44491
  Copyright terms: Public domain W3C validator