Theorem pweqd 4271

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 4269	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1596  𝒫 cpw 4266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-in 3687  df-ss 3694  df-pw 4268

This theorem is referenced by:  undefval  7522  pmvalg  7985  marypha1lem  8455  marypha1  8456  r1val3  8814  ackbij1lem5  9159  ackbij2lem2  9175  ackbij2lem3  9176  r1om  9179  isfin2  9229  hsmexlem8  9359  vdwmc  15805  hashbcval  15829  ismre  16373  mrcfval  16391  mrisval  16413  mreexexlemd  16427  brssc  16596  lubfval  17100  glbfval  17113  isclat  17231  issubm  17469  issubg  17716  cntzfval  17874  symgval  17920  lsmfval  18174  lsmpropd  18211  pj1fval  18228  issubrg  18903  lssset  19057  lspfval  19096  lsppropd  19141  islbs  19199  sraval  19299  aspval  19451  opsrval  19597  ply1frcl  19806  evls1fval  19807  ocvfval  20133  isobs  20187  islinds  20271  basis1  20877  baspartn  20881  cldval  20950  ntrfval  20951  clsfval  20952  mretopd  21019  neifval  21026  lpfval  21065  cncls2  21200  iscnrm  21250  iscnrm2  21265  2ndcsep  21385  kgenval  21461  xkoval  21513  dfac14  21544  qtopval  21621  qtopval2  21622  isfbas  21755  trfbas2  21769  flimval  21889  elflim  21897  flimclslem  21910  fclsfnflim  21953  fclscmp  21956  tsmsfbas  22053  tsmsval2  22055  ustval  22128  utopval  22158  mopnfss  22370  setsmstopn  22405  met2ndc  22450  istrkgb  25474  isuhgr  26075  isushgr  26076  isuhgrop  26085  uhgrun  26089  uhgrstrrepe  26093  isupgr  26099  upgrop  26109  isumgr  26110  upgrun  26133  umgrun  26135  isuspgr  26167  isusgr  26168  isuspgrop  26176  isusgrop  26177  ausgrusgrb  26180  usgrstrrepe  26247  issubgr  26283  uhgrspansubgrlem  26302  usgrexi  26468  1hevtxdg1  26533  umgr2v2e  26552  ismeas  30492  omsval  30585  omscl  30587  omsf  30588  oms0  30589  carsgval  30595  omsmeas  30615  erdszelem3  31403  erdsze  31412  kur14  31426  iscvm  31469  mpstval  31660  mclsval  31688  madeval  32162  heibor  33852  idlval  34044  igenval  34092  paddfval  35503  pclfvalN  35595  polfvalN  35610  docaffvalN  36829  docafvalN  36830  djaffvalN  36841  djafvalN  36842  dochffval  37057  dochfval  37058  djhffval  37104  djhfval  37105  lpolsetN  37190  lcdlss2N  37328  mzpclval  37707  dfac21  38055  islmodfg  38058  islssfg  38059  rgspnval  38157  rfovd  38714  fsovrfovd  38722  gneispace2  38849  sge0val  41003  ismea  41088  psmeasure  41108  caragenval  41130  isome  41131  omeunile  41142  isomennd  41168  ovnval  41178  hspmbl  41266  isvonmbl  41275  issubmgm  42216  lincop  42624  lcoop  42627  islininds  42662  ldepsnlinc  42724