Theorem pweq 4546

Description: Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 13-Apr-2024.)

Assertion

Ref	Expression
pweq	⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Proof of Theorem pweq

Step	Hyp	Ref	Expression
1		eqimss 3973	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4545	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3974	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4545	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3934	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1539  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  pweqi  4548  pweqd  4549  axpweq  5282  pwexg  5296  pwssun  5476  knatar  7208  pwdom  8865  canth2g  8867  pwfi  8923  pwfiOLD  9044  fival  9101  marypha1lem  9122  marypha1  9123  wdompwdom  9267  canthwdom  9268  r1sucg  9458  ranklim  9533  r1pwALT  9535  isacn  9731  dfac12r  9833  dfac12k  9834  pwsdompw  9891  ackbij1lem8  9914  ackbij1lem14  9920  r1om  9931  fictb  9932  isfin1a  9979  isfin2  9981  isfin3  9983  isfin3ds  10016  isf33lem  10053  domtriomlem  10129  ttukeylem1  10196  elgch  10309  wunpw  10394  wunex2  10425  wuncval2  10434  eltskg  10437  eltsk2g  10438  tskpwss  10439  tskpw  10440  inar1  10462  grupw  10482  grothpw  10513  grothpwex  10514  axgroth6  10515  grothomex  10516  grothac  10517  axdc4uz  13632  hashpw  14079  hashbc  14093  ackbijnn  15468  incexclem  15476  rami  16644  ismre  17216  isacs  17277  isacs2  17279  acsfiel  17280  isacs1i  17283  mreacs  17284  isssc  17449  acsficl  18180  efmnd  18424  pmtrfval  18973  selvffval  21236  istopg  21952  istopon  21969  eltg  22015  tgdom  22036  ntrval  22095  nrmsep3  22414  iscmp  22447  cmpcov  22448  cmpsublem  22458  cmpsub  22459  tgcmp  22460  uncmp  22462  hauscmplem  22465  is1stc  22500  2ndc1stc  22510  llyi  22533  nllyi  22534  cldllycmp  22554  isfbas  22888  isfil  22906  filss  22912  fgval  22929  elfg  22930  isufil  22962  alexsublem  23103  alexsubb  23105  alexsubALTlem1  23106  alexsubALTlem2  23107  alexsubALTlem4  23109  alexsubALT  23110  restmetu  23632  bndth  24027  ovolicc2  24591  uhgreq12g  27338  uhgr0vb  27345  isupgr  27357  isumgr  27368  isuspgr  27425  isusgr  27426  isausgr  27437  lfuhgr1v0e  27524  usgrexmpl  27533  nbuhgr2vtx1edgblem  27621  ex-pw  28694  iscref  31696  indv  31880  sigaval  31979  issiga  31980  isrnsiga  31981  issgon  31991  isldsys  32024  issros  32043  measval  32066  isrnmeas  32068  rankpwg  34398  neibastop1  34475  neibastop2lem  34476  neibastop2  34477  neibastop3  34478  neifg  34487  limsucncmpi  34561  bj-snglex  35090  bj-ismoore  35203  pibp19  35512  pibt2  35515  cover2g  35800  isnacs  40442  mrefg2  40445  aomclem8  40802  islssfg2  40812  lnr2i  40857  pwelg  41056  fsovd  41505  fsovcnvlem  41510  dssmapfvd  41514  clsk1independent  41545  ntrneibex  41572  mnuop123d  41769  stoweidlem50  43481  stoweidlem57  43488  issal  43745  omessle  43926  vsetrec  46294  elpglem3  46304