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

Theorem pweq 4538
Description: Equality theorem for power class. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
pweq (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Proof of Theorem pweq
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 sseq2 3990 . . 3 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21abbidv 2882 . 2 (𝐴 = 𝐵 → {𝑥𝑥𝐴} = {𝑥𝑥𝐵})
3 df-pw 4537 . 2 𝒫 𝐴 = {𝑥𝑥𝐴}
4 df-pw 4537 . 2 𝒫 𝐵 = {𝑥𝑥𝐵}
52, 3, 43eqtr4g 2878 1 (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  {cab 2796  wss 3933  𝒫 cpw 4535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949  df-pw 4537
This theorem is referenced by:  pweqi  4539  pweqd  4540  axpweq  5256  pwexg  5270  pwssun  5448  knatar  7099  pwdom  8657  canth2g  8659  pwfi  8807  fival  8864  marypha1lem  8885  marypha1  8886  wdompwdom  9030  canthwdom  9031  r1sucg  9186  ranklim  9261  r1pwALT  9263  isacn  9458  dfac12r  9560  dfac12k  9561  pwsdompw  9614  ackbij1lem8  9637  ackbij1lem14  9643  r1om  9654  fictb  9655  isfin1a  9702  isfin2  9704  isfin3  9706  isfin3ds  9739  isf33lem  9776  domtriomlem  9852  ttukeylem1  9919  elgch  10032  wunpw  10117  wunex2  10148  wuncval2  10157  eltskg  10160  eltsk2g  10161  tskpwss  10162  tskpw  10163  inar1  10185  grupw  10205  grothpw  10236  grothpwex  10237  axgroth6  10238  grothomex  10239  grothac  10240  axdc4uz  13340  hashpw  13785  hashbc  13799  ackbijnn  15171  incexclem  15179  rami  16339  ismre  16849  isacs  16910  isacs2  16912  acsfiel  16913  isacs1i  16916  mreacs  16917  isssc  17078  acsficl  17769  pmtrfval  18507  selvffval  20257  istopg  21431  istopon  21448  eltg  21493  tgdom  21514  ntrval  21572  nrmsep3  21891  iscmp  21924  cmpcov  21925  cmpsublem  21935  cmpsub  21936  tgcmp  21937  uncmp  21939  hauscmplem  21942  is1stc  21977  2ndc1stc  21987  llyi  22010  nllyi  22011  cldllycmp  22031  isfbas  22365  isfil  22383  filss  22389  fgval  22406  elfg  22407  isufil  22439  alexsublem  22580  alexsubb  22582  alexsubALTlem1  22583  alexsubALTlem2  22584  alexsubALTlem4  22586  alexsubALT  22587  restmetu  23107  bndth  23489  ovolicc2  24050  uhgreq12g  26777  uhgr0vb  26784  isupgr  26796  isumgr  26807  isuspgr  26864  isusgr  26865  isausgr  26876  lfuhgr1v0e  26963  usgrexmpl  26972  nbuhgr2vtx1edgblem  27060  ex-pw  28135  iscref  31007  indv  31170  sigaval  31269  issiga  31270  isrnsiga  31271  issgon  31281  isldsys  31314  issros  31333  measval  31356  isrnmeas  31358  rankpwg  33527  neibastop1  33604  neibastop2lem  33605  neibastop2  33606  neibastop3  33607  neifg  33616  limsucncmpi  33690  bj-snglex  34182  bj-ismoore  34291  pibp19  34577  pibt2  34580  cover2g  34871  isnacs  39179  mrefg2  39182  aomclem8  39539  islssfg2  39549  lnr2i  39594  pwelg  39797  fsovd  40232  fsovcnvlem  40237  dssmapfvd  40241  clsk1independent  40274  ntrneibex  40301  mnuop123d  40475  stoweidlem50  42212  stoweidlem57  42219  issal  42476  omessle  42657  efmnd  43969  vsetrec  44733  elpglem3  44743
  Copyright terms: Public domain W3C validator