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

Theorem pweq 4194
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 3660 . . 3 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21abbidv 2770 . 2 (𝐴 = 𝐵 → {𝑥𝑥𝐴} = {𝑥𝑥𝐵})
3 df-pw 4193 . 2 𝒫 𝐴 = {𝑥𝑥𝐴}
4 df-pw 4193 . 2 𝒫 𝐵 = {𝑥𝑥𝐵}
52, 3, 43eqtr4g 2710 1 (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  {cab 2637  wss 3607  𝒫 cpw 4191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-pw 4193
This theorem is referenced by:  pweqi  4195  pweqd  4196  axpweq  4872  pwex  4878  pwexg  4880  pwssun  5049  knatar  6647  pwdom  8153  canth2g  8155  pwfi  8302  fival  8359  marypha1lem  8380  marypha1  8381  wdompwdom  8524  canthwdom  8525  r1sucg  8670  ranklim  8745  r1pwALT  8747  isacn  8905  dfac12r  9006  dfac12k  9007  pwsdompw  9064  ackbij1lem5  9084  ackbij1lem8  9087  ackbij1lem14  9093  r1om  9104  fictb  9105  isfin1a  9152  isfin2  9154  isfin3  9156  isfin3ds  9189  isf33lem  9226  domtriomlem  9302  ttukeylem1  9369  elgch  9482  wunpw  9567  wunex2  9598  wuncval2  9607  eltskg  9610  eltsk2g  9611  tskpwss  9612  tskpw  9613  inar1  9635  grupw  9655  grothpw  9686  grothpwex  9687  axgroth6  9688  grothomex  9689  grothac  9690  axdc4uz  12823  hashpw  13261  hashbc  13275  ackbijnn  14604  incexclem  14612  rami  15766  ismre  16297  isacs  16359  isacs2  16361  acsfiel  16362  isacs1i  16365  mreacs  16366  isssc  16527  acsficl  17218  pmtrfval  17916  istopg  20748  istopon  20765  eltg  20809  tgdom  20830  ntrval  20888  nrmsep3  21207  iscmp  21239  cmpcov  21240  cmpsublem  21250  cmpsub  21251  tgcmp  21252  uncmp  21254  hauscmplem  21257  is1stc  21292  2ndc1stc  21302  llyi  21325  nllyi  21326  cldllycmp  21346  isfbas  21680  isfil  21698  filss  21704  fgval  21721  elfg  21722  isufil  21754  alexsublem  21895  alexsubb  21897  alexsubALTlem1  21898  alexsubALTlem2  21899  alexsubALTlem4  21901  alexsubALT  21902  restmetu  22422  bndth  22804  ovolicc2  23336  uhgreq12g  26005  uhgr0vb  26012  isupgr  26024  isumgr  26035  isuspgr  26092  isusgr  26093  isausgr  26104  lfuhgr1v0e  26191  usgrexmpl  26200  nbuhgr2vtx1edgblem  26292  ex-pw  27416  iscref  30039  indv  30202  sigaval  30301  issiga  30302  isrnsigaOLD  30303  isrnsiga  30304  issgon  30314  isldsys  30347  issros  30366  measval  30389  isrnmeas  30391  rankpwg  32401  neibastop1  32479  neibastop2lem  32480  neibastop2  32481  neibastop3  32482  neifg  32491  limsucncmpi  32569  bj-snglex  33086  bj-ismoore  33184  cover2g  33639  isnacs  37584  mrefg2  37587  aomclem8  37948  islssfg2  37958  lnr2i  38003  pwelg  38182  fsovd  38619  fsovcnvlem  38624  dssmapfvd  38628  clsk1independent  38661  ntrneibex  38688  stoweidlem50  40585  stoweidlem57  40592  issal  40852  omessle  41033  vsetrec  42774  elpglem3  42784
  Copyright terms: Public domain W3C validator