Theorem pweqd 4573

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-pw 4558

This theorem is used by:  undefval  8302  pmvalg  8865  marypha1lem  9432  marypha1  9433  r1val3  9857  ackbij2lem2  10324  ackbij2lem3  10325  hfom  10328  isfin2  10379  hsmexlem8  10509  vdwmc  17165  hashbcval  17189  ismre  17769  mrcfval  17791  mrisval  17813  mreexexlemd  17827  brssc  17998  lubfval  18531  glbfval  18544  isclat  18683  issubmgm  18900  issubm  19007  issubg  19345  cntzfval  19543  lsmfval  19861  lsmpropd  19900  pj1fval  19917  issubrng  20808  issubrg  20832  rgspnval  20873  lssset  21217  lspfval  21257  lsppropd  21302  islbs  21360  sraval  21459  ocvfval  21981  isobs  22035  islinds  22124  aspval  22189  opsrval  22364  ply1frcl  22645  evls1fval  22646  basis1  23277  baspartn  23281  cldval  23350  ntrfval  23351  clsfval  23352  mretopd  23419  neifval  23426  lpfval  23465  cncls2  23600  iscnrm  23650  iscnrm2  23665  2ndcsep  23787  kgenval  23863  xkoval  23915  dfac14  23946  qtopval  24023  qtopval2  24024  isfbas  24157  trfbas2  24171  flimval  24291  elflim  24299  flimclslem  24312  fclsfnflim  24355  fclscmp  24358  tsmsfbas  24456  tsmsval2  24458  ustval  24531  utopval  24560  mopnfss  24771  setsmstopn  24806  met2ndc  24851  madeval  28227  elmade2  28253  istrkgb  28926  isuhgr  29647  isushgr  29648  isuhgrop  29657  uhgrun  29661  uhgrstrrepe  29665  isupgr  29671  upgrop  29681  isumgr  29682  upgrun  29705  umgrun  29707  isuspgr  29742  isusgr  29743  isuspgrop  29751  isusgrop  29752  ausgrusgrb  29755  usgrstrrepe  29825  issubgr  29861  uhgrspansubgrlem  29880  usgrexi  30031  1hevtxdg1  30096  umgr2v2e  30115  zarcmplem  34563  ismeas  34882  omsval  34975  omscl  34977  omsf  34978  oms0  34979  carsgval  34985  omsmeas  35005  erdszelem3  36076  erdsze  36085  kur14  36099  iscvm  36142  mpstval  36418  mclsval  36446  mh-infprim2bi  37459  bj-imdirvallem  38238  pibp21  38475  heibor  38892  idlval  39084  igenval  39132  paddfval  40991  pclfvalN  41083  polfvalN  41098  docaffvalN  42315  docafvalN  42316  djaffvalN  42327  djafvalN  42328  dochffval  42543  dochfval  42544  djhffval  42590  djhfval  42591  lpolsetN  42676  lcdlss2N  42814  mzpclval  43873  dfac21  44205  islmodfg  44208  islssfg  44209  rfovd  45138  fsovrfovd  45146  gneispace2  45269  ismnu  45382  sge0val  47512  ismea  47597  psmeasure  47617  caragenval  47639  isome  47640  omeunile  47651  isomennd  47677  ovnval  47687  hspmbl  47775  isvonmbl  47784  afv2eq12d  48421  isisubgr  49096  isubgruhgr  49102  stgrfv  49187  stgrusgra  49193  gpgov  49276  gpgusgra  49291  lincop  49656  lcoop  49659  islininds  49694  ldepsnlinc  49756  isclatd  50233