Theorem pweq 4382

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.

Step	Hyp	Ref	Expression
1		sseq2 3846	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵))
2	1	abbidv 2906	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 ⊆ 𝐴} = {𝑥 ∣ 𝑥 ⊆ 𝐵})
3		df-pw 4381	. 2 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}
4		df-pw 4381	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
5	2, 3, 4	3eqtr4g 2839	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1601  {cab 2763   ⊆ wss 3792  𝒫 cpw 4379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-in 3799  df-ss 3806  df-pw 4381

This theorem is referenced by:  pweqi  4383  pweqd  4384  axpweq  5076  pwexg  5090  pwssun  5257  knatar  6879  pwdom  8400  canth2g  8402  pwfi  8549  fival  8606  marypha1lem  8627  marypha1  8628  wdompwdom  8772  canthwdom  8773  r1sucg  8929  ranklim  9004  r1pwALT  9006  isacn  9200  dfac12r  9303  dfac12k  9304  pwsdompw  9361  ackbij1lem8  9384  ackbij1lem14  9390  r1om  9401  fictb  9402  isfin1a  9449  isfin2  9451  isfin3  9453  isfin3ds  9486  isf33lem  9523  domtriomlem  9599  ttukeylem1  9666  elgch  9779  wunpw  9864  wunex2  9895  wuncval2  9904  eltskg  9907  eltsk2g  9908  tskpwss  9909  tskpw  9910  inar1  9932  grupw  9952  grothpw  9983  grothpwex  9984  axgroth6  9985  grothomex  9986  grothac  9987  axdc4uz  13102  hashpw  13537  hashbc  13551  ackbijnn  14964  incexclem  14972  rami  16123  ismre  16636  isacs  16697  isacs2  16699  acsfiel  16700  isacs1i  16703  mreacs  16704  isssc  16865  acsficl  17557  pmtrfval  18253  istopg  21107  istopon  21124  eltg  21169  tgdom  21190  ntrval  21248  nrmsep3  21567  iscmp  21600  cmpcov  21601  cmpsublem  21611  cmpsub  21612  tgcmp  21613  uncmp  21615  hauscmplem  21618  is1stc  21653  2ndc1stc  21663  llyi  21686  nllyi  21687  cldllycmp  21707  isfbas  22041  isfil  22059  filss  22065  fgval  22082  elfg  22083  isufil  22115  alexsublem  22256  alexsubb  22258  alexsubALTlem1  22259  alexsubALTlem2  22260  alexsubALTlem4  22262  alexsubALT  22263  restmetu  22783  bndth  23165  ovolicc2  23726  uhgreq12g  26413  uhgr0vb  26420  isupgr  26432  isumgr  26443  isuspgr  26501  isusgr  26502  isausgr  26513  lfuhgr1v0e  26601  usgrexmpl  26610  nbuhgr2vtx1edgblem  26698  ex-pw  27861  iscref  30509  indv  30672  sigaval  30771  issiga  30772  isrnsigaOLD  30773  isrnsiga  30774  issgon  30784  isldsys  30817  issros  30836  measval  30859  isrnmeas  30861  rankpwg  32865  neibastop1  32942  neibastop2lem  32943  neibastop2  32944  neibastop3  32945  neifg  32954  limsucncmpi  33027  bj-snglex  33533  bj-ismoore  33632  cover2g  34134  isnacs  38227  mrefg2  38230  aomclem8  38590  islssfg2  38600  lnr2i  38645  pwelg  38822  fsovd  39258  fsovcnvlem  39263  dssmapfvd  39267  clsk1independent  39300  ntrneibex  39327  stoweidlem50  41194  stoweidlem57  41201  issal  41458  omessle  41639  vsetrec  43554  elpglem3  43564