Theorem pweq 4617

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  pweqi  4619  pweqd  4620  axpweq  5349  pwexg  5377  pwssun  5572  knatar  7354  pwdom  9129  canth2g  9131  pwfi  9178  pwfiOLD  9347  fival  9407  marypha1lem  9428  marypha1  9429  wdompwdom  9573  canthwdom  9574  r1sucg  9764  ranklim  9839  r1pwALT  9841  isacn  10039  dfac12r  10141  dfac12k  10142  pwsdompw  10199  ackbij1lem8  10222  ackbij1lem14  10228  r1om  10239  fictb  10240  isfin1a  10287  isfin2  10289  isfin3  10291  isfin3ds  10324  isf33lem  10361  domtriomlem  10437  ttukeylem1  10504  elgch  10617  wunpw  10702  wunex2  10733  wuncval2  10742  eltskg  10745  eltsk2g  10746  tskpwss  10747  tskpw  10748  inar1  10770  grupw  10790  grothpw  10821  grothpwex  10822  axgroth6  10823  grothomex  10824  grothac  10825  axdc4uz  13949  hashpw  14396  hashbc  14412  ackbijnn  15774  incexclem  15782  rami  16948  ismre  17534  isacs  17595  isacs2  17597  acsfiel  17598  isacs1i  17601  mreacs  17602  isssc  17767  acsficl  18500  efmnd  18751  pmtrfval  19318  selvffval  21679  istopg  22397  istopon  22414  eltg  22460  tgdom  22481  ntrval  22540  nrmsep3  22859  iscmp  22892  cmpcov  22893  cmpsublem  22903  cmpsub  22904  tgcmp  22905  uncmp  22907  hauscmplem  22910  is1stc  22945  2ndc1stc  22955  llyi  22978  nllyi  22979  cldllycmp  22999  isfbas  23333  isfil  23351  filss  23357  fgval  23374  elfg  23375  isufil  23407  alexsublem  23548  alexsubb  23550  alexsubALTlem1  23551  alexsubALTlem2  23552  alexsubALTlem4  23554  alexsubALT  23555  restmetu  24079  bndth  24474  ovolicc2  25039  uhgreq12g  28325  uhgr0vb  28332  isupgr  28344  isumgr  28355  isuspgr  28412  isusgr  28413  isausgr  28424  lfuhgr1v0e  28511  usgrexmpl  28520  nbuhgr2vtx1edgblem  28608  ex-pw  29682  iscref  32824  indv  33010  sigaval  33109  issiga  33110  isrnsiga  33111  issgon  33121  isldsys  33154  issros  33173  measval  33196  isrnmeas  33198  rankpwg  35141  neibastop1  35244  neibastop2lem  35245  neibastop2  35246  neibastop3  35247  neifg  35256  limsucncmpi  35330  bj-snglex  35854  bj-ismoore  35986  pibp19  36295  pibt2  36298  cover2g  36584  isnacs  41442  mrefg2  41445  aomclem8  41803  islssfg2  41813  lnr2i  41858  pwelg  42311  fsovd  42759  fsovcnvlem  42764  dssmapfvd  42768  clsk1independent  42797  ntrneibex  42824  mnuop123d  43021  stoweidlem50  44766  stoweidlem57  44773  issal  45030  omessle  45214  vsetrec  47748  elpglem3  47758  pgindnf  47761