Theorem pweqd 4163

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

Step	Hyp	Ref	Expression
1		pweqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		pweq 4161	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1483  𝒫 cpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  undefval  7402  pmvalg  7868  marypha1lem  8339  marypha1  8340  r1val3  8701  ackbij1lem5  9046  ackbij2lem2  9062  ackbij2lem3  9063  r1om  9066  isfin2  9116  hsmexlem8  9246  vdwmc  15682  hashbcval  15706  ismre  16250  mrcfval  16268  mrisval  16290  mreexexlemd  16304  brssc  16474  lubfval  16978  glbfval  16991  isclat  17109  issubm  17347  issubg  17594  cntzfval  17753  symgval  17799  lsmfval  18053  lsmpropd  18090  pj1fval  18107  issubrg  18780  lssset  18934  lspfval  18973  lsppropd  19018  islbs  19076  sraval  19176  aspval  19328  opsrval  19474  ply1frcl  19683  evls1fval  19684  ocvfval  20010  isobs  20064  islinds  20148  basis1  20754  baspartn  20758  cldval  20827  ntrfval  20828  clsfval  20829  mretopd  20896  neifval  20903  lpfval  20942  cncls2  21077  iscnrm  21127  iscnrm2  21142  2ndcsep  21262  kgenval  21338  xkoval  21390  dfac14  21421  qtopval  21498  qtopval2  21499  isfbas  21633  trfbas2  21647  flimval  21767  elflim  21775  flimclslem  21788  fclsfnflim  21831  fclscmp  21834  tsmsfbas  21931  tsmsval2  21933  ustval  22006  utopval  22036  mopnfss  22248  setsmstopn  22283  met2ndc  22328  istrkgb  25354  isuhgr  25955  isushgr  25956  isuhgrop  25965  uhgrun  25969  uhgrstrrepe  25973  isupgr  25979  upgrop  25989  isumgr  25990  upgrun  26013  umgrun  26015  isuspgr  26047  isusgr  26048  isuspgrop  26056  isusgrop  26057  ausgrusgrb  26060  usgrstrrepe  26127  issubgr  26163  uhgrspansubgrlem  26182  usgrexi  26337  1hevtxdg1  26402  umgr2v2e  26421  ismeas  30262  omsval  30355  omscl  30357  omsf  30358  oms0  30359  carsgval  30365  omsmeas  30385  erdszelem3  31175  erdsze  31184  kur14  31198  iscvm  31241  mpstval  31432  mclsval  31460  madeval  31935  heibor  33620  idlval  33812  igenval  33860  paddfval  35083  pclfvalN  35175  polfvalN  35190  docaffvalN  36410  docafvalN  36411  djaffvalN  36422  djafvalN  36423  dochffval  36638  dochfval  36639  djhffval  36685  djhfval  36686  lpolsetN  36771  lcdlss2N  36909  mzpclval  37288  dfac21  37636  islmodfg  37639  islssfg  37640  rgspnval  37738  rfovd  38295  fsovrfovd  38303  gneispace2  38430  sge0val  40583  ismea  40668  psmeasure  40688  caragenval  40707  isome  40708  omeunile  40719  isomennd  40745  ovnval  40755  hspmbl  40843  isvonmbl  40852  issubmgm  41789  lincop  42197  lcoop  42200  islininds  42235  ldepsnlinc  42297