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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-pw 4559

This theorem is used by:  undefval  8276  pmvalg  8837  marypha1lem  9404  marypha1  9405  r1val3  9821  ackbij2lem2  10242  ackbij2lem3  10243  r1om  10246  isfin2  10297  hsmexlem8  10427  vdwmc  17071  hashbcval  17095  ismre  17675  mrcfval  17697  mrisval  17719  mreexexlemd  17733  brssc  17904  lubfval  18437  glbfval  18450  isclat  18589  issubmgm  18805  issubm  18912  issubg  19250  cntzfval  19448  lsmfval  19766  lsmpropd  19805  pj1fval  19822  issubrng  20710  issubrg  20734  rgspnval  20775  lssset  21118  lspfval  21158  lsppropd  21203  islbs  21261  sraval  21360  ocvfval  21880  isobs  21934  islinds  22023  aspval  22088  opsrval  22263  ply1frcl  22544  evls1fval  22545  basis1  23176  baspartn  23180  cldval  23249  ntrfval  23250  clsfval  23251  mretopd  23318  neifval  23325  lpfval  23364  cncls2  23499  iscnrm  23549  iscnrm2  23564  2ndcsep  23686  kgenval  23762  xkoval  23814  dfac14  23845  qtopval  23922  qtopval2  23923  isfbas  24056  trfbas2  24070  flimval  24190  elflim  24198  flimclslem  24211  fclsfnflim  24254  fclscmp  24257  tsmsfbas  24355  tsmsval2  24357  ustval  24430  utopval  24459  mopnfss  24670  setsmstopn  24705  met2ndc  24750  madeval  28098  elmade2  28124  istrkgb  28797  isuhgr  29518  isushgr  29519  isuhgrop  29528  uhgrun  29532  uhgrstrrepe  29536  isupgr  29542  upgrop  29552  isumgr  29553  upgrun  29576  umgrun  29578  isuspgr  29613  isusgr  29614  isuspgrop  29622  isusgrop  29623  ausgrusgrb  29626  usgrstrrepe  29696  issubgr  29732  uhgrspansubgrlem  29751  usgrexi  29902  1hevtxdg1  29967  umgr2v2e  29986  zarcmplem  34392  ismeas  34711  omsval  34805  omscl  34807  omsf  34808  oms0  34809  carsgval  34815  omsmeas  34835  erdszelem3  35773  erdsze  35782  kur14  35796  iscvm  35839  mpstval  36115  mclsval  36143  mh-infprim2bi  37167  bj-imdirvallem  37933  pibp21  38170  heibor  38572  idlval  38764  igenval  38812  paddfval  40671  pclfvalN  40763  polfvalN  40778  docaffvalN  41995  docafvalN  41996  djaffvalN  42007  djafvalN  42008  dochffval  42223  dochfval  42224  djhffval  42270  djhfval  42271  lpolsetN  42356  lcdlss2N  42494  mzpclval  43571  dfac21  43908  islmodfg  43911  islssfg  43912  rfovd  44842  fsovrfovd  44850  gneispace2  44973  ismnu  45086  sge0val  47195  ismea  47280  psmeasure  47300  caragenval  47322  isome  47323  omeunile  47334  isomennd  47360  ovnval  47370  hspmbl  47458  isvonmbl  47467  afv2eq12d  48104  isisubgr  48779  isubgruhgr  48785  stgrfv  48870  stgrusgra  48876  gpgov  48959  gpgusgra  48974  lincop  49339  lcoop  49342  islininds  49377  ldepsnlinc  49439  isclatd  49910