Theorem pweq 4614

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-pw 4602

This theorem is referenced by:  pweqi  4616  pweqd  4617  axpweq  5351  pwexg  5378  pwssun  5575  knatar  7377  pwdom  9169  canth2g  9171  pwfi  9357  fival  9452  marypha1lem  9473  marypha1  9474  wdompwdom  9618  canthwdom  9619  r1sucg  9809  ranklim  9884  r1pwALT  9886  isacn  10084  dfac12r  10187  dfac12k  10188  pwsdompw  10243  ackbij1lem8  10266  ackbij1lem14  10272  r1om  10283  fictb  10284  isfin1a  10332  isfin2  10334  isfin3  10336  isfin3ds  10369  isf33lem  10406  domtriomlem  10482  ttukeylem1  10549  elgch  10662  wunpw  10747  wunex2  10778  wuncval2  10787  eltskg  10790  eltsk2g  10791  tskpwss  10792  tskpw  10793  inar1  10815  grupw  10835  grothpw  10866  grothpwex  10867  axgroth6  10868  grothomex  10869  grothac  10870  axdc4uz  14025  hashpw  14475  hashbc  14492  ackbijnn  15864  incexclem  15872  rami  17053  ismre  17633  isacs  17694  isacs2  17696  acsfiel  17697  isacs1i  17700  mreacs  17701  isssc  17864  acsficl  18592  efmnd  18883  pmtrfval  19468  selvffval  22137  istopg  22901  istopon  22918  eltg  22964  tgdom  22985  ntrval  23044  nrmsep3  23363  iscmp  23396  cmpcov  23397  cmpsublem  23407  cmpsub  23408  tgcmp  23409  uncmp  23411  hauscmplem  23414  is1stc  23449  2ndc1stc  23459  llyi  23482  nllyi  23483  cldllycmp  23503  isfbas  23837  isfil  23855  filss  23861  fgval  23878  elfg  23879  isufil  23911  alexsublem  24052  alexsubb  24054  alexsubALTlem1  24055  alexsubALTlem2  24056  alexsubALTlem4  24058  alexsubALT  24059  restmetu  24583  bndth  24990  ovolicc2  25557  uhgreq12g  29082  uhgr0vb  29089  isupgr  29101  isumgr  29112  isuspgr  29169  isusgr  29170  isausgr  29181  lfuhgr1v0e  29271  nbuhgr2vtx1edgblem  29368  ex-pw  30448  indv  32837  iscref  33843  sigaval  34112  issiga  34113  isrnsiga  34114  issgon  34124  isldsys  34157  issros  34176  measval  34199  isrnmeas  34201  rankpwg  36170  neibastop1  36360  neibastop2lem  36361  neibastop2  36362  neibastop3  36363  neifg  36372  limsucncmpi  36446  bj-snglex  36974  bj-ismoore  37106  pibp19  37415  pibt2  37418  cover2g  37723  isnacs  42715  mrefg2  42718  aomclem8  43073  islssfg2  43083  lnr2i  43128  pwelg  43573  fsovd  44021  fsovcnvlem  44026  dssmapfvd  44030  clsk1independent  44059  ntrneibex  44086  mnuop123d  44281  stoweidlem50  46065  stoweidlem57  46072  issal  46329  omessle  46513  grtri  47907  vsetrec  49222  elpglem3  49232  pgindnf  49235