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  5288  pwexg  5315  pwssun  5516  knatar  7305  pwdom  9060  canth2g  9062  pwfi  9222  fival  9318  marypha1lem  9339  marypha1  9340  wdompwdom  9486  canthwdom  9487  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  10536  wunpw  10621  wunex2  10652  wuncval2  10661  eltskg  10664  eltsk2g  10665  tskpwss  10666  tskpw  10667  inar1  10689  grupw  10709  grothpw  10740  grothpwex  10741  axgroth6  10742  grothomex  10743  grothac  10744  indv  12152  axdc4uz  13937  hashpw  14389  hashbc  14406  ackbijnn  15784  incexclem  15792  rami  16977  ismre  17543  isacs  17608  isacs2  17610  acsfiel  17611  isacs1i  17614  mreacs  17615  isssc  17778  acsficl  18504  efmnd  18829  pmtrfval  19416  selvffval  22109  istopg  22870  istopon  22887  eltg  22932  tgdom  22953  ntrval  23011  nrmsep3  23330  iscmp  23363  cmpcov  23364  cmpsublem  23374  cmpsub  23375  tgcmp  23376  uncmp  23378  hauscmplem  23381  is1stc  23416  2ndc1stc  23426  llyi  23449  nllyi  23450  cldllycmp  23470  isfbas  23804  isfil  23822  filss  23828  fgval  23845  elfg  23846  isufil  23878  alexsublem  24019  alexsubb  24021  alexsubALTlem1  24022  alexsubALTlem2  24023  alexsubALTlem4  24025  alexsubALT  24026  restmetu  24545  bndth  24935  ovolicc2  25499  uhgreq12g  29148  uhgr0vb  29155  isupgr  29167  isumgr  29178  isuspgr  29235  isusgr  29236  isausgr  29247  lfuhgr1v0e  29337  nbuhgr2vtx1edgblem  29434  ex-pw  30514  esplyval  33721  iscref  34004  sigaval  34271  issiga  34272  isrnsiga  34273  issgon  34283  isldsys  34316  issros  34335  measval  34358  isrnmeas  34360  rankpwg  36367  neibastop1  36557  neibastop2lem  36558  neibastop2  36559  neibastop3  36560  neifg  36569  limsucncmpi  36643  bj-snglex  37296  bj-ismoore  37433  pibp19  37744  pibt2  37747  cover2g  38051  isnacs  43150  mrefg2  43153  aomclem8  43507  islssfg2  43517  lnr2i  43562  pwelg  44005  fsovd  44453  fsovcnvlem  44458  dssmapfvd  44462  clsk1independent  44491  ntrneibex  44518  mnuop123d  44707  stoweidlem50  46496  stoweidlem57  46503  issal  46760  omessle  46944  grtri  48428  vsetrec  50190  elpglem3  50200  pgindnf  50203