Theorem pweq 4513

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 3971	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4512	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3972	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4512	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3932	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1538  𝒫 cpw 4497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  pweqi  4515  pweqd  4516  axpweq  5230  pwexg  5244  pwssun  5421  knatar  7089  pwdom  8653  canth2g  8655  pwfi  8803  fival  8860  marypha1lem  8881  marypha1  8882  wdompwdom  9026  canthwdom  9027  r1sucg  9182  ranklim  9257  r1pwALT  9259  isacn  9455  dfac12r  9557  dfac12k  9558  pwsdompw  9615  ackbij1lem8  9638  ackbij1lem14  9644  r1om  9655  fictb  9656  isfin1a  9703  isfin2  9705  isfin3  9707  isfin3ds  9740  isf33lem  9777  domtriomlem  9853  ttukeylem1  9920  elgch  10033  wunpw  10118  wunex2  10149  wuncval2  10158  eltskg  10161  eltsk2g  10162  tskpwss  10163  tskpw  10164  inar1  10186  grupw  10206  grothpw  10237  grothpwex  10238  axgroth6  10239  grothomex  10240  grothac  10241  axdc4uz  13347  hashpw  13793  hashbc  13807  ackbijnn  15175  incexclem  15183  rami  16341  ismre  16853  isacs  16914  isacs2  16916  acsfiel  16917  isacs1i  16920  mreacs  16921  isssc  17082  acsficl  17773  efmnd  18027  pmtrfval  18570  selvffval  20788  istopg  21500  istopon  21517  eltg  21562  tgdom  21583  ntrval  21641  nrmsep3  21960  iscmp  21993  cmpcov  21994  cmpsublem  22004  cmpsub  22005  tgcmp  22006  uncmp  22008  hauscmplem  22011  is1stc  22046  2ndc1stc  22056  llyi  22079  nllyi  22080  cldllycmp  22100  isfbas  22434  isfil  22452  filss  22458  fgval  22475  elfg  22476  isufil  22508  alexsublem  22649  alexsubb  22651  alexsubALTlem1  22652  alexsubALTlem2  22653  alexsubALTlem4  22655  alexsubALT  22656  restmetu  23177  bndth  23563  ovolicc2  24126  uhgreq12g  26858  uhgr0vb  26865  isupgr  26877  isumgr  26888  isuspgr  26945  isusgr  26946  isausgr  26957  lfuhgr1v0e  27044  usgrexmpl  27053  nbuhgr2vtx1edgblem  27141  ex-pw  28214  iscref  31197  indv  31381  sigaval  31480  issiga  31481  isrnsiga  31482  issgon  31492  isldsys  31525  issros  31544  measval  31567  isrnmeas  31569  rankpwg  33743  neibastop1  33820  neibastop2lem  33821  neibastop2  33822  neibastop3  33823  neifg  33832  limsucncmpi  33906  bj-snglex  34409  bj-ismoore  34520  pibp19  34831  pibt2  34834  cover2g  35153  isnacs  39645  mrefg2  39648  aomclem8  40005  islssfg2  40015  lnr2i  40060  pwelg  40259  fsovd  40709  fsovcnvlem  40714  dssmapfvd  40718  clsk1independent  40749  ntrneibex  40776  mnuop123d  40970  stoweidlem50  42692  stoweidlem57  42699  issal  42956  omessle  43137  vsetrec  45232  elpglem3  45242