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

Theorem pweq 4354
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 3824 . . 3 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21abbidv 2925 . 2 (𝐴 = 𝐵 → {𝑥𝑥𝐴} = {𝑥𝑥𝐵})
3 df-pw 4353 . 2 𝒫 𝐴 = {𝑥𝑥𝐴}
4 df-pw 4353 . 2 𝒫 𝐵 = {𝑥𝑥𝐵}
52, 3, 43eqtr4g 2865 1 (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  {cab 2792  wss 3769  𝒫 cpw 4351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783  df-pw 4353
This theorem is referenced by:  pweqi  4355  pweqd  4356  axpweq  5034  pwexg  5048  pwssun  5215  knatar  6827  pwdom  8347  canth2g  8349  pwfi  8496  fival  8553  marypha1lem  8574  marypha1  8575  wdompwdom  8718  canthwdom  8719  r1sucg  8875  ranklim  8950  r1pwALT  8952  isacn  9146  dfac12r  9249  dfac12k  9250  pwsdompw  9307  ackbij1lem8  9330  ackbij1lem14  9336  r1om  9347  fictb  9348  isfin1a  9395  isfin2  9397  isfin3  9399  isfin3ds  9432  isf33lem  9469  domtriomlem  9545  ttukeylem1  9612  elgch  9725  wunpw  9810  wunex2  9841  wuncval2  9850  eltskg  9853  eltsk2g  9854  tskpwss  9855  tskpw  9856  inar1  9878  grupw  9898  grothpw  9929  grothpwex  9930  axgroth6  9931  grothomex  9932  grothac  9933  axdc4uz  13003  hashpw  13436  hashbc  13450  ackbijnn  14778  incexclem  14786  rami  15932  ismre  16451  isacs  16512  isacs2  16514  acsfiel  16515  isacs1i  16518  mreacs  16519  isssc  16680  acsficl  17372  pmtrfval  18067  istopg  20909  istopon  20926  eltg  20971  tgdom  20992  ntrval  21050  nrmsep3  21369  iscmp  21401  cmpcov  21402  cmpsublem  21412  cmpsub  21413  tgcmp  21414  uncmp  21416  hauscmplem  21419  is1stc  21454  2ndc1stc  21464  llyi  21487  nllyi  21488  cldllycmp  21508  isfbas  21842  isfil  21860  filss  21866  fgval  21883  elfg  21884  isufil  21916  alexsublem  22057  alexsubb  22059  alexsubALTlem1  22060  alexsubALTlem2  22061  alexsubALTlem4  22063  alexsubALT  22064  restmetu  22584  bndth  22966  ovolicc2  23499  uhgreq12g  26170  uhgr0vb  26177  isupgr  26189  isumgr  26200  isuspgr  26258  isusgr  26259  isausgr  26270  lfuhgr1v0e  26358  usgrexmpl  26367  nbuhgr2vtx1edgblem  26459  ex-pw  27613  iscref  30232  indv  30395  sigaval  30494  issiga  30495  isrnsigaOLD  30496  isrnsiga  30497  issgon  30507  isldsys  30540  issros  30559  measval  30582  isrnmeas  30584  rankpwg  32592  neibastop1  32670  neibastop2lem  32671  neibastop2  32672  neibastop3  32673  neifg  32682  limsucncmpi  32756  bj-snglex  33266  bj-ismoore  33365  cover2g  33816  isnacs  37763  mrefg2  37766  aomclem8  38126  islssfg2  38136  lnr2i  38181  pwelg  38359  fsovd  38796  fsovcnvlem  38801  dssmapfvd  38805  clsk1independent  38838  ntrneibex  38865  stoweidlem50  40740  stoweidlem57  40747  issal  41007  omessle  41188  vsetrec  43011  elpglem3  43021
  Copyright terms: Public domain W3C validator