Theorem pweq 4620

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 4040	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4619	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 4041	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4619	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3999	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1533  𝒫 cpw 4606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-in 3956  df-ss 3966  df-pw 4608

This theorem is referenced by:  pweqi  4622  pweqd  4623  axpweq  5354  pwexg  5382  pwssun  5577  knatar  7371  pwdom  9160  canth2g  9162  pwfi  9209  pwfiOLD  9379  fival  9443  marypha1lem  9464  marypha1  9465  wdompwdom  9609  canthwdom  9610  r1sucg  9800  ranklim  9875  r1pwALT  9877  isacn  10075  dfac12r  10177  dfac12k  10178  pwsdompw  10235  ackbij1lem8  10258  ackbij1lem14  10264  r1om  10275  fictb  10276  isfin1a  10323  isfin2  10325  isfin3  10327  isfin3ds  10360  isf33lem  10397  domtriomlem  10473  ttukeylem1  10540  elgch  10653  wunpw  10738  wunex2  10769  wuncval2  10778  eltskg  10781  eltsk2g  10782  tskpwss  10783  tskpw  10784  inar1  10806  grupw  10826  grothpw  10857  grothpwex  10858  axgroth6  10859  grothomex  10860  grothac  10861  axdc4uz  13989  hashpw  14435  hashbc  14452  ackbijnn  15814  incexclem  15822  rami  16991  ismre  17577  isacs  17638  isacs2  17640  acsfiel  17641  isacs1i  17644  mreacs  17645  isssc  17810  acsficl  18546  efmnd  18829  pmtrfval  19412  selvffval  22066  istopg  22817  istopon  22834  eltg  22880  tgdom  22901  ntrval  22960  nrmsep3  23279  iscmp  23312  cmpcov  23313  cmpsublem  23323  cmpsub  23324  tgcmp  23325  uncmp  23327  hauscmplem  23330  is1stc  23365  2ndc1stc  23375  llyi  23398  nllyi  23399  cldllycmp  23419  isfbas  23753  isfil  23771  filss  23777  fgval  23794  elfg  23795  isufil  23827  alexsublem  23968  alexsubb  23970  alexsubALTlem1  23971  alexsubALTlem2  23972  alexsubALTlem4  23974  alexsubALT  23975  restmetu  24499  bndth  24904  ovolicc2  25471  uhgreq12g  28898  uhgr0vb  28905  isupgr  28917  isumgr  28928  isuspgr  28985  isusgr  28986  isausgr  28997  lfuhgr1v0e  29087  usgrexmpl  29096  nbuhgr2vtx1edgblem  29184  ex-pw  30259  iscref  33478  indv  33664  sigaval  33763  issiga  33764  isrnsiga  33765  issgon  33775  isldsys  33808  issros  33827  measval  33850  isrnmeas  33852  rankpwg  35798  neibastop1  35876  neibastop2lem  35877  neibastop2  35878  neibastop3  35879  neifg  35888  limsucncmpi  35962  bj-snglex  36485  bj-ismoore  36617  pibp19  36926  pibt2  36929  cover2g  37222  isnacs  42155  mrefg2  42158  aomclem8  42516  islssfg2  42526  lnr2i  42571  pwelg  43021  fsovd  43469  fsovcnvlem  43474  dssmapfvd  43478  clsk1independent  43507  ntrneibex  43534  mnuop123d  43730  stoweidlem50  45467  stoweidlem57  45474  issal  45731  omessle  45915  vsetrec  48212  elpglem3  48222  pgindnf  48225