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

Theorem pweqd 4557
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 4554 . 2 (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
31, 2syl 17 1 (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  𝒫 cpw 4538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951  df-pw 4540
This theorem is referenced by:  undefval  7941  pmvalg  8416  marypha1lem  8896  marypha1  8897  r1val3  9266  ackbij2lem2  9661  ackbij2lem3  9662  r1om  9665  isfin2  9715  hsmexlem8  9845  vdwmc  16313  hashbcval  16337  ismre  16860  mrcfval  16878  mrisval  16900  mreexexlemd  16914  brssc  17083  lubfval  17587  glbfval  17600  isclat  17718  issubm  17967  issubg  18278  cntzfval  18449  lsmfval  18762  lsmpropd  18802  pj1fval  18819  issubrg  19534  lssset  19704  lspfval  19744  lsppropd  19789  islbs  19847  sraval  19947  aspval  20101  opsrval  20254  ply1frcl  20480  evls1fval  20481  ocvfval  20809  isobs  20863  islinds  20952  basis1  21557  baspartn  21561  cldval  21630  ntrfval  21631  clsfval  21632  mretopd  21699  neifval  21706  lpfval  21745  cncls2  21880  iscnrm  21930  iscnrm2  21945  2ndcsep  22066  kgenval  22142  xkoval  22194  dfac14  22225  qtopval  22302  qtopval2  22303  isfbas  22436  trfbas2  22450  flimval  22570  elflim  22578  flimclslem  22591  fclsfnflim  22634  fclscmp  22637  tsmsfbas  22735  tsmsval2  22737  ustval  22810  utopval  22840  mopnfss  23052  setsmstopn  23087  met2ndc  23132  istrkgb  26240  isuhgr  26844  isushgr  26845  isuhgrop  26854  uhgrun  26858  uhgrstrrepe  26862  isupgr  26868  upgrop  26878  isumgr  26879  upgrun  26902  umgrun  26904  isuspgr  26936  isusgr  26937  isuspgrop  26945  isusgrop  26946  ausgrusgrb  26949  usgrstrrepe  27016  issubgr  27052  uhgrspansubgrlem  27071  usgrexi  27222  1hevtxdg1  27287  umgr2v2e  27306  ismeas  31458  omsval  31551  omscl  31553  omsf  31554  oms0  31555  carsgval  31561  omsmeas  31581  erdszelem3  32440  erdsze  32449  kur14  32463  iscvm  32506  mpstval  32782  mclsval  32810  madeval  33289  bj-imdirval  34471  pibp21  34695  heibor  35098  idlval  35290  igenval  35338  paddfval  36932  pclfvalN  37024  polfvalN  37039  docaffvalN  38256  docafvalN  38257  djaffvalN  38268  djafvalN  38269  dochffval  38484  dochfval  38485  djhffval  38531  djhfval  38532  lpolsetN  38617  lcdlss2N  38755  mzpclval  39320  dfac21  39664  islmodfg  39667  islssfg  39668  rgspnval  39766  rfovd  40345  fsovrfovd  40353  gneispace2  40480  ismnu  40595  sge0val  42647  ismea  42732  psmeasure  42752  caragenval  42774  isome  42775  omeunile  42786  isomennd  42812  ovnval  42822  hspmbl  42910  isvonmbl  42919  afv2eq12d  43413  issubmgm  44055  lincop  44462  lcoop  44465  islininds  44500  ldepsnlinc  44562
  Copyright terms: Public domain W3C validator