MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pweqd Structured version   Visualization version   GIF version

Theorem pweqd 4555
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
StepHypRef Expression
1 pweqd.1 . 2 (𝜑𝐴 = 𝐵)
2 pweq 4552 . 2 (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
31, 2syl 17 1 (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  𝒫 cpw 4538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-ext 2706
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1541  df-ex 1779  df-sb 2065  df-clab 2713  df-cleq 2727  df-clel 2813  df-v 3438  df-in 3898  df-ss 3908  df-pw 4540
This theorem is referenced by:  undefval  8127  pmvalg  8662  marypha1lem  9250  marypha1  9251  r1val3  9654  ackbij2lem2  10056  ackbij2lem3  10057  r1om  10060  isfin2  10110  hsmexlem8  10240  vdwmc  16738  hashbcval  16762  ismre  17358  mrcfval  17376  mrisval  17398  mreexexlemd  17412  brssc  17585  lubfval  18127  glbfval  18140  isclat  18277  issubm  18501  issubg  18814  cntzfval  18985  lsmfval  19302  lsmpropd  19342  pj1fval  19359  issubrg  20087  lssset  20258  lspfval  20298  lsppropd  20343  islbs  20401  sraval  20501  ocvfval  20934  isobs  20990  islinds  21079  aspval  21140  opsrval  21310  ply1frcl  21547  evls1fval  21548  basis1  22163  baspartn  22167  cldval  22237  ntrfval  22238  clsfval  22239  mretopd  22306  neifval  22313  lpfval  22352  cncls2  22487  iscnrm  22537  iscnrm2  22552  2ndcsep  22673  kgenval  22749  xkoval  22801  dfac14  22832  qtopval  22909  qtopval2  22910  isfbas  23043  trfbas2  23057  flimval  23177  elflim  23185  flimclslem  23198  fclsfnflim  23241  fclscmp  23244  tsmsfbas  23342  tsmsval2  23344  ustval  23417  utopval  23447  mopnfss  23659  setsmstopn  23696  met2ndc  23742  istrkgb  26914  isuhgr  27528  isushgr  27529  isuhgrop  27538  uhgrun  27542  uhgrstrrepe  27546  isupgr  27552  upgrop  27562  isumgr  27563  upgrun  27586  umgrun  27588  isuspgr  27620  isusgr  27621  isuspgrop  27629  isusgrop  27630  ausgrusgrb  27633  usgrstrrepe  27700  issubgr  27736  uhgrspansubgrlem  27755  usgrexi  27906  1hevtxdg1  27971  umgr2v2e  27990  zarcmplem  31927  ismeas  32263  omsval  32356  omscl  32358  omsf  32359  oms0  32360  carsgval  32366  omsmeas  32386  erdszelem3  33251  erdsze  33260  kur14  33274  iscvm  33317  mpstval  33593  mclsval  33621  madeval  34095  elmade2  34111  bj-imdirvallem  35409  pibp21  35644  heibor  36037  idlval  36229  igenval  36277  paddfval  38021  pclfvalN  38113  polfvalN  38128  docaffvalN  39345  docafvalN  39346  djaffvalN  39357  djafvalN  39358  dochffval  39573  dochfval  39574  djhffval  39620  djhfval  39621  lpolsetN  39706  lcdlss2N  39844  mzpclval  40755  dfac21  41100  islmodfg  41103  islssfg  41104  rgspnval  41202  rfovd  41835  fsovrfovd  41843  gneispace2  41968  ismnu  42105  sge0val  44147  ismea  44232  psmeasure  44252  caragenval  44274  isome  44275  omeunile  44286  isomennd  44312  ovnval  44322  hspmbl  44410  isvonmbl  44419  afv2eq12d  44964  issubmgm  45600  lincop  46006  lcoop  46009  islininds  46044  ldepsnlinc  46106  isclatd  46526
  Copyright terms: Public domain W3C validator