Theorem pweq 4567

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 3996	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4566	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3997	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4566	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3955	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1540  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-pw 4555

This theorem is referenced by:  pweqi  4569  pweqd  4570  axpweq  5293  pwexg  5320  pwssun  5515  knatar  7298  pwdom  9053  canth2g  9055  pwfi  9226  fival  9321  marypha1lem  9342  marypha1  9343  wdompwdom  9489  canthwdom  9490  r1sucg  9684  ranklim  9759  r1pwALT  9761  isacn  9957  dfac12r  10060  dfac12k  10061  pwsdompw  10116  ackbij1lem8  10139  ackbij1lem14  10145  r1om  10156  fictb  10157  isfin1a  10205  isfin2  10207  isfin3  10209  isfin3ds  10242  isf33lem  10279  domtriomlem  10355  ttukeylem1  10422  elgch  10535  wunpw  10620  wunex2  10651  wuncval2  10660  eltskg  10663  eltsk2g  10664  tskpwss  10665  tskpw  10666  inar1  10688  grupw  10708  grothpw  10739  grothpwex  10740  axgroth6  10741  grothomex  10742  grothac  10743  axdc4uz  13910  hashpw  14362  hashbc  14379  ackbijnn  15754  incexclem  15762  rami  16946  ismre  17511  isacs  17576  isacs2  17578  acsfiel  17579  isacs1i  17582  mreacs  17583  isssc  17746  acsficl  18472  efmnd  18763  pmtrfval  19348  selvffval  22037  istopg  22799  istopon  22816  eltg  22861  tgdom  22882  ntrval  22940  nrmsep3  23259  iscmp  23292  cmpcov  23293  cmpsublem  23303  cmpsub  23304  tgcmp  23305  uncmp  23307  hauscmplem  23310  is1stc  23345  2ndc1stc  23355  llyi  23378  nllyi  23379  cldllycmp  23399  isfbas  23733  isfil  23751  filss  23757  fgval  23774  elfg  23775  isufil  23807  alexsublem  23948  alexsubb  23950  alexsubALTlem1  23951  alexsubALTlem2  23952  alexsubALTlem4  23954  alexsubALT  23955  restmetu  24475  bndth  24874  ovolicc2  25440  uhgreq12g  29029  uhgr0vb  29036  isupgr  29048  isumgr  29059  isuspgr  29116  isusgr  29117  isausgr  29128  lfuhgr1v0e  29218  nbuhgr2vtx1edgblem  29315  ex-pw  30392  indv  32814  iscref  33830  sigaval  34097  issiga  34098  isrnsiga  34099  issgon  34109  isldsys  34142  issros  34161  measval  34184  isrnmeas  34186  rankpwg  36162  neibastop1  36352  neibastop2lem  36353  neibastop2  36354  neibastop3  36355  neifg  36364  limsucncmpi  36438  bj-snglex  36966  bj-ismoore  37098  pibp19  37407  pibt2  37410  cover2g  37715  isnacs  42697  mrefg2  42700  aomclem8  43054  islssfg2  43064  lnr2i  43109  pwelg  43553  fsovd  44001  fsovcnvlem  44006  dssmapfvd  44010  clsk1independent  44039  ntrneibex  44066  mnuop123d  44255  stoweidlem50  46051  stoweidlem57  46058  issal  46315  omessle  46499  grtri  47944  vsetrec  49708  elpglem3  49718  pgindnf  49721