Theorem pweq 4565

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 3989	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4564	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3990	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4564	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3948	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1541  𝒫 cpw 4551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-pw 4553

This theorem is referenced by:  pweqi  4567  pweqd  4568  axpweq  5293  pwexg  5320  pwssun  5513  knatar  7300  pwdom  9053  canth2g  9055  pwfi  9214  fival  9307  marypha1lem  9328  marypha1  9329  wdompwdom  9475  canthwdom  9476  r1sucg  9673  ranklim  9748  r1pwALT  9750  isacn  9946  dfac12r  10049  dfac12k  10050  pwsdompw  10105  ackbij1lem8  10128  ackbij1lem14  10134  r1om  10145  fictb  10146  isfin1a  10194  isfin2  10196  isfin3  10198  isfin3ds  10231  isf33lem  10268  domtriomlem  10344  ttukeylem1  10411  elgch  10524  wunpw  10609  wunex2  10640  wuncval2  10649  eltskg  10652  eltsk2g  10653  tskpwss  10654  tskpw  10655  inar1  10677  grupw  10697  grothpw  10728  grothpwex  10729  axgroth6  10730  grothomex  10731  grothac  10732  axdc4uz  13898  hashpw  14350  hashbc  14367  ackbijnn  15742  incexclem  15750  rami  16934  ismre  17500  isacs  17565  isacs2  17567  acsfiel  17568  isacs1i  17571  mreacs  17572  isssc  17735  acsficl  18461  efmnd  18786  pmtrfval  19370  selvffval  22067  istopg  22830  istopon  22847  eltg  22892  tgdom  22913  ntrval  22971  nrmsep3  23290  iscmp  23323  cmpcov  23324  cmpsublem  23334  cmpsub  23335  tgcmp  23336  uncmp  23338  hauscmplem  23341  is1stc  23376  2ndc1stc  23386  llyi  23409  nllyi  23410  cldllycmp  23430  isfbas  23764  isfil  23782  filss  23788  fgval  23805  elfg  23806  isufil  23838  alexsublem  23979  alexsubb  23981  alexsubALTlem1  23982  alexsubALTlem2  23983  alexsubALTlem4  23985  alexsubALT  23986  restmetu  24505  bndth  24904  ovolicc2  25470  uhgreq12g  29064  uhgr0vb  29071  isupgr  29083  isumgr  29094  isuspgr  29151  isusgr  29152  isausgr  29163  lfuhgr1v0e  29253  nbuhgr2vtx1edgblem  29350  ex-pw  30430  indv  32859  esplyval  33648  iscref  33929  sigaval  34196  issiga  34197  isrnsiga  34198  issgon  34208  isldsys  34241  issros  34260  measval  34283  isrnmeas  34285  rankpwg  36285  neibastop1  36475  neibastop2lem  36476  neibastop2  36477  neibastop3  36478  neifg  36487  limsucncmpi  36561  bj-snglex  37090  bj-ismoore  37222  pibp19  37531  pibt2  37534  cover2g  37829  isnacs  42861  mrefg2  42864  aomclem8  43218  islssfg2  43228  lnr2i  43273  pwelg  43717  fsovd  44165  fsovcnvlem  44170  dssmapfvd  44174  clsk1independent  44203  ntrneibex  44230  mnuop123d  44419  stoweidlem50  46210  stoweidlem57  46217  issal  46474  omessle  46658  grtri  48102  vsetrec  49864  elpglem3  49874  pgindnf  49877