Theorem pweqd 4574

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-pw 4559

This theorem is used by:  undefval  8294  pmvalg  8857  marypha1lem  9425  marypha1  9426  r1val3  9850  ackbij2lem2  10317  ackbij2lem3  10318  hfom  10321  isfin2  10372  hsmexlem8  10502  vdwmc  17156  hashbcval  17180  ismre  17760  mrcfval  17782  mrisval  17804  mreexexlemd  17818  brssc  17989  lubfval  18522  glbfval  18535  isclat  18674  issubmgm  18891  issubm  18998  issubg  19336  cntzfval  19534  lsmfval  19852  lsmpropd  19891  pj1fval  19908  issubrng  20799  issubrg  20823  rgspnval  20864  lssset  21208  lspfval  21248  lsppropd  21293  islbs  21351  sraval  21450  ocvfval  21972  isobs  22026  islinds  22115  aspval  22180  opsrval  22355  ply1frcl  22636  evls1fval  22637  basis1  23268  baspartn  23272  cldval  23341  ntrfval  23342  clsfval  23343  mretopd  23410  neifval  23417  lpfval  23456  cncls2  23591  iscnrm  23641  iscnrm2  23656  2ndcsep  23778  kgenval  23854  xkoval  23906  dfac14  23937  qtopval  24014  qtopval2  24015  isfbas  24148  trfbas2  24162  flimval  24282  elflim  24290  flimclslem  24303  fclsfnflim  24346  fclscmp  24349  tsmsfbas  24447  tsmsval2  24449  ustval  24522  utopval  24551  mopnfss  24762  setsmstopn  24797  met2ndc  24842  madeval  28218  elmade2  28244  istrkgb  28917  isuhgr  29638  isushgr  29639  isuhgrop  29648  uhgrun  29652  uhgrstrrepe  29656  isupgr  29662  upgrop  29672  isumgr  29673  upgrun  29696  umgrun  29698  isuspgr  29733  isusgr  29734  isuspgrop  29742  isusgrop  29743  ausgrusgrb  29746  usgrstrrepe  29816  issubgr  29852  uhgrspansubgrlem  29871  usgrexi  30022  1hevtxdg1  30087  umgr2v2e  30106  zarcmplem  34513  ismeas  34832  omsval  34925  omscl  34927  omsf  34928  oms0  34929  carsgval  34935  omsmeas  34955  erdszelem3  35958  erdsze  35967  kur14  35981  iscvm  36024  mpstval  36300  mclsval  36328  mh-infprim2bi  37335  bj-imdirvallem  38101  pibp21  38338  heibor  38755  idlval  38947  igenval  38995  paddfval  40854  pclfvalN  40946  polfvalN  40961  docaffvalN  42178  docafvalN  42179  djaffvalN  42190  djafvalN  42191  dochffval  42406  dochfval  42407  djhffval  42453  djhfval  42454  lpolsetN  42539  lcdlss2N  42677  mzpclval  43735  dfac21  44067  islmodfg  44070  islssfg  44071  rfovd  45000  fsovrfovd  45008  gneispace2  45131  ismnu  45244  sge0val  47375  ismea  47460  psmeasure  47480  caragenval  47502  isome  47503  omeunile  47514  isomennd  47540  ovnval  47550  hspmbl  47638  isvonmbl  47647  afv2eq12d  48284  isisubgr  48959  isubgruhgr  48965  stgrfv  49050  stgrusgra  49056  gpgov  49139  gpgusgra  49154  lincop  49519  lcoop  49522  islininds  49557  ldepsnlinc  49619  isclatd  50090