Theorem pweqd 4584

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

Syntax hints:   → wi 4   = wceq 1567  𝒫 cpw 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-pw 4569

This theorem is referenced by:  undefval  8273  pmvalg  8834  marypha1lem  9393  marypha1  9394  r1val3  9810  ackbij2lem2  10222  ackbij2lem3  10223  r1om  10226  isfin2  10278  hsmexlem8  10408  vdwmc  17038  hashbcval  17062  ismre  17642  mrcfval  17664  mrisval  17686  mreexexlemd  17700  brssc  17871  lubfval  18404  glbfval  18417  isclat  18556  issubmgm  18760  issubm  18861  issubg  19192  cntzfval  19390  lsmfval  19708  lsmpropd  19747  pj1fval  19764  issubrng  20632  issubrg  20656  rgspnval  20697  lssset  21032  lspfval  21072  lsppropd  21117  islbs  21175  sraval  21274  ocvfval  21785  isobs  21839  islinds  21928  aspval  21991  opsrval  22166  ply1frcl  22447  evls1fval  22448  basis1  23076  baspartn  23080  cldval  23149  ntrfval  23150  clsfval  23151  mretopd  23218  neifval  23225  lpfval  23264  cncls2  23399  iscnrm  23449  iscnrm2  23464  2ndcsep  23585  kgenval  23661  xkoval  23713  dfac14  23744  qtopval  23821  qtopval2  23822  isfbas  23955  trfbas2  23969  flimval  24089  elflim  24097  flimclslem  24110  fclsfnflim  24153  fclscmp  24156  tsmsfbas  24254  tsmsval2  24256  ustval  24329  utopval  24358  mopnfss  24569  setsmstopn  24604  met2ndc  24649  madeval  27991  elmade2  28017  istrkgb  28690  isuhgr  29351  isushgr  29352  isuhgrop  29361  uhgrun  29365  uhgrstrrepe  29369  isupgr  29375  upgrop  29385  isumgr  29386  upgrun  29409  umgrun  29411  isuspgr  29443  isusgr  29444  isuspgrop  29452  isusgrop  29453  ausgrusgrb  29456  usgrstrrepe  29526  issubgr  29562  uhgrspansubgrlem  29581  usgrexi  29732  1hevtxdg1  29797  umgr2v2e  29816  zarcmplem  34216  ismeas  34534  omsval  34628  omscl  34630  omsf  34631  oms0  34632  carsgval  34638  omsmeas  34658  erdszelem3  35584  erdsze  35593  kur14  35607  iscvm  35650  mpstval  35926  mclsval  35954  mh-infprim2bi  36947  bj-imdirvallem  37712  pibp21  37949  heibor  38360  idlval  38552  igenval  38600  paddfval  40461  pclfvalN  40553  polfvalN  40568  docaffvalN  41785  docafvalN  41786  djaffvalN  41797  djafvalN  41798  dochffval  42013  dochfval  42014  djhffval  42060  djhfval  42061  lpolsetN  42146  lcdlss2N  42284  mzpclval  43348  dfac21  43685  islmodfg  43688  islssfg  43689  rfovd  44619  fsovrfovd  44627  gneispace2  44750  ismnu  44863  sge0val  46972  ismea  47057  psmeasure  47077  caragenval  47099  isome  47100  omeunile  47111  isomennd  47137  ovnval  47147  hspmbl  47235  isvonmbl  47244  afv2eq12d  47841  isisubgr  48516  isubgruhgr  48522  stgrfv  48607  stgrusgra  48613  gpgov  48696  gpgusgra  48711  lincop  49073  lcoop  49076  islininds  49111  ldepsnlinc  49173  isclatd  49646