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

Theorem pweq 4110
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 3589 . . 3 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21abbidv 2727 . 2 (𝐴 = 𝐵 → {𝑥𝑥𝐴} = {𝑥𝑥𝐵})
3 df-pw 4109 . 2 𝒫 𝐴 = {𝑥𝑥𝐴}
4 df-pw 4109 . 2 𝒫 𝐵 = {𝑥𝑥𝐵}
52, 3, 43eqtr4g 2668 1 (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  {cab 2595  wss 3539  𝒫 cpw 4107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553  df-pw 4109
This theorem is referenced by:  pweqi  4111  pweqd  4112  axpweq  4762  pwex  4768  pwexg  4770  pwssun  4933  knatar  6484  pwdom  7974  canth2g  7976  pwfi  8121  fival  8178  marypha1lem  8199  marypha1  8200  wdompwdom  8343  canthwdom  8344  r1sucg  8492  ranklim  8567  r1pwALT  8569  isacn  8727  dfac12r  8828  dfac12k  8829  pwsdompw  8886  ackbij1lem5  8906  ackbij1lem8  8909  ackbij1lem14  8915  r1om  8926  fictb  8927  isfin1a  8974  isfin2  8976  isfin3  8978  isfin3ds  9011  isf33lem  9048  domtriomlem  9124  ttukeylem1  9191  elgch  9300  wunpw  9385  wunex2  9416  wuncval2  9425  eltskg  9428  eltsk2g  9429  tskpwss  9430  tskpw  9431  inar1  9453  grupw  9473  grothpw  9504  grothpwex  9505  axgroth6  9506  grothomex  9507  grothac  9508  axdc4uz  12602  hashpw  13037  hashbc  13048  ackbijnn  14347  incexclem  14355  rami  15505  ismre  16021  isacs  16083  isacs2  16085  acsfiel  16086  isacs1i  16089  mreacs  16090  isssc  16251  acsficl  16942  pmtrfval  17641  istopg  20472  istopon  20487  eltg  20519  tgdom  20540  ntrval  20597  nrmsep3  20916  iscmp  20948  cmpcov  20949  cmpsublem  20959  cmpsub  20960  tgcmp  20961  uncmp  20963  hauscmplem  20966  is1stc  21001  2ndc1stc  21011  llyi  21034  nllyi  21035  cldllycmp  21055  isfbas  21390  isfil  21408  filss  21414  fgval  21431  elfg  21432  isufil  21464  alexsublem  21605  alexsubb  21607  alexsubALTlem1  21608  alexsubALTlem2  21609  alexsubALTlem4  21611  alexsubALT  21612  restmetu  22132  bndth  22512  ovolicc2  23041  isuhgra  25620  isushgra  25623  uhgrac  25627  uhgraeq12d  25629  isausgra  25676  usgraeq12d  25684  ex-pw  26471  iscref  29032  indv  29195  sigaval  29293  issiga  29294  isrnsigaOLD  29295  isrnsiga  29296  issgon  29306  isldsys  29339  issros  29358  measval  29381  isrnmeas  29383  rankpwg  31239  neibastop1  31317  neibastop2lem  31318  neibastop2  31319  neibastop3  31320  neifg  31329  limsucncmpi  31407  bj-snglex  31937  cover2g  32462  isnacs  36068  mrefg2  36071  aomclem8  36432  islssfg2  36442  lnr2i  36488  pwelg  36667  fsovd  37105  fsovcnvlem  37110  dssmapfvd  37114  clsk1independent  37147  ntrneibex  37174  stoweidlem50  38726  stoweidlem57  38733  issal  38993  omessle  39171  uhgreq12g  40268  uhgruhgra  40273  uhgrauhgr  40274  uhgr0vb  40278  isupgr  40291  isumgr  40301  isuspgr  40363  isusgr  40364  isausgr  40375  lfuhgr1v0e  40461  usgrexmpl  40468  nbuhgr2vtx1edgblem  40554
  Copyright terms: Public domain W3C validator