Theorem pweqd 4620

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

Syntax hints:   → wi 4   = wceq 1534  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964  df-pw 4605

This theorem is referenced by:  undefval  8281  pmvalg  8855  marypha1lem  9456  marypha1  9457  r1val3  9861  ackbij2lem2  10263  ackbij2lem3  10264  r1om  10267  isfin2  10317  hsmexlem8  10447  vdwmc  16946  hashbcval  16970  ismre  17569  mrcfval  17587  mrisval  17609  mreexexlemd  17623  brssc  17796  lubfval  18341  glbfval  18354  isclat  18491  issubmgm  18661  issubm  18754  issubg  19080  cntzfval  19270  lsmfval  19592  lsmpropd  19631  pj1fval  19648  issubrng  20483  issubrg  20509  lssset  20816  lspfval  20856  lsppropd  20902  islbs  20960  sraval  21059  ocvfval  21597  isobs  21653  islinds  21742  aspval  21805  opsrval  21983  ply1frcl  22236  evls1fval  22237  basis1  22852  baspartn  22856  cldval  22926  ntrfval  22927  clsfval  22928  mretopd  22995  neifval  23002  lpfval  23041  cncls2  23176  iscnrm  23226  iscnrm2  23241  2ndcsep  23362  kgenval  23438  xkoval  23490  dfac14  23521  qtopval  23598  qtopval2  23599  isfbas  23732  trfbas2  23746  flimval  23866  elflim  23874  flimclslem  23887  fclsfnflim  23930  fclscmp  23933  tsmsfbas  24031  tsmsval2  24033  ustval  24106  utopval  24136  mopnfss  24348  setsmstopn  24385  met2ndc  24431  madeval  27778  elmade2  27794  istrkgb  28258  isuhgr  28872  isushgr  28873  isuhgrop  28882  uhgrun  28886  uhgrstrrepe  28890  isupgr  28896  upgrop  28906  isumgr  28907  upgrun  28930  umgrun  28932  isuspgr  28964  isusgr  28965  isuspgrop  28973  isusgrop  28974  ausgrusgrb  28977  usgrstrrepe  29047  issubgr  29083  uhgrspansubgrlem  29102  usgrexi  29253  1hevtxdg1  29319  umgr2v2e  29338  zarcmplem  33482  ismeas  33818  omsval  33913  omscl  33915  omsf  33916  oms0  33917  carsgval  33923  omsmeas  33943  erdszelem3  34803  erdsze  34812  kur14  34826  iscvm  34869  mpstval  35145  mclsval  35173  bj-imdirvallem  36659  pibp21  36894  heibor  37294  idlval  37486  igenval  37534  paddfval  39270  pclfvalN  39362  polfvalN  39377  docaffvalN  40594  docafvalN  40595  djaffvalN  40606  djafvalN  40607  dochffval  40822  dochfval  40823  djhffval  40869  djhfval  40870  lpolsetN  40955  lcdlss2N  41093  mzpclval  42145  dfac21  42490  islmodfg  42493  islssfg  42494  rgspnval  42592  rfovd  43431  fsovrfovd  43439  gneispace2  43562  ismnu  43698  sge0val  45754  ismea  45839  psmeasure  45859  caragenval  45881  isome  45882  omeunile  45893  isomennd  45919  ovnval  45929  hspmbl  46017  isvonmbl  46026  afv2eq12d  46595  lincop  47476  lcoop  47479  islininds  47514  ldepsnlinc  47576  isclatd  47994

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »