Theorem pweq 4556

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 3981	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4555	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3982	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4555	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3940	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1542  𝒫 cpw 4542

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-pw 4544

This theorem is referenced by:  pweqi  4558  pweqd  4559  axpweq  5286  pwexg  5313  pwssun  5514  knatar  7303  pwdom  9058  canth2g  9060  pwfi  9220  fival  9316  marypha1lem  9337  marypha1  9338  wdompwdom  9484  canthwdom  9485  r1sucg  9682  ranklim  9757  r1pwALT  9759  isacn  9955  dfac12r  10058  dfac12k  10059  pwsdompw  10114  ackbij1lem8  10137  ackbij1lem14  10143  r1om  10154  fictb  10155  isfin1a  10203  isfin2  10205  isfin3  10207  isfin3ds  10240  isf33lem  10277  domtriomlem  10353  ttukeylem1  10420  elgch  10534  wunpw  10619  wunex2  10650  wuncval2  10659  eltskg  10662  eltsk2g  10663  tskpwss  10664  tskpw  10665  inar1  10687  grupw  10707  grothpw  10738  grothpwex  10739  axgroth6  10740  grothomex  10741  grothac  10742  indv  12150  axdc4uz  13935  hashpw  14387  hashbc  14404  ackbijnn  15782  incexclem  15790  rami  16975  ismre  17541  isacs  17606  isacs2  17608  acsfiel  17609  isacs1i  17612  mreacs  17613  isssc  17776  acsficl  18502  efmnd  18827  pmtrfval  19414  selvffval  22108  istopg  22869  istopon  22886  eltg  22931  tgdom  22952  ntrval  23010  nrmsep3  23329  iscmp  23362  cmpcov  23363  cmpsublem  23373  cmpsub  23374  tgcmp  23375  uncmp  23377  hauscmplem  23380  is1stc  23415  2ndc1stc  23425  llyi  23448  nllyi  23449  cldllycmp  23469  isfbas  23803  isfil  23821  filss  23827  fgval  23844  elfg  23845  isufil  23877  alexsublem  24018  alexsubb  24020  alexsubALTlem1  24021  alexsubALTlem2  24022  alexsubALTlem4  24024  alexsubALT  24025  restmetu  24544  bndth  24934  ovolicc2  25498  uhgreq12g  29153  uhgr0vb  29160  isupgr  29172  isumgr  29183  isuspgr  29240  isusgr  29241  isausgr  29252  lfuhgr1v0e  29342  nbuhgr2vtx1edgblem  29439  ex-pw  30519  esplyval  33726  iscref  34009  sigaval  34276  issiga  34277  isrnsiga  34278  issgon  34288  isldsys  34321  issros  34340  measval  34363  isrnmeas  34365  rankpwg  36372  neibastop1  36562  neibastop2lem  36563  neibastop2  36564  neibastop3  36565  neifg  36574  limsucncmpi  36648  bj-snglex  37293  bj-ismoore  37430  pibp19  37741  pibt2  37744  cover2g  38048  isnacs  43147  mrefg2  43150  aomclem8  43504  islssfg2  43514  lnr2i  43559  pwelg  44002  fsovd  44450  fsovcnvlem  44455  dssmapfvd  44459  clsk1independent  44488  ntrneibex  44515  mnuop123d  44704  stoweidlem50  46493  stoweidlem57  46500  issal  46757  omessle  46941  grtri  48413  vsetrec  50175  elpglem3  50185  pgindnf  50188