Theorem pweq 4619

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 4054	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4618	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 4055	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4618	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 4013	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1537  𝒫 cpw 4605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-pw 4607

This theorem is referenced by:  pweqi  4621  pweqd  4622  axpweq  5357  pwexg  5384  pwssun  5580  knatar  7377  pwdom  9168  canth2g  9170  pwfi  9355  fival  9450  marypha1lem  9471  marypha1  9472  wdompwdom  9616  canthwdom  9617  r1sucg  9807  ranklim  9882  r1pwALT  9884  isacn  10082  dfac12r  10185  dfac12k  10186  pwsdompw  10241  ackbij1lem8  10264  ackbij1lem14  10270  r1om  10281  fictb  10282  isfin1a  10330  isfin2  10332  isfin3  10334  isfin3ds  10367  isf33lem  10404  domtriomlem  10480  ttukeylem1  10547  elgch  10660  wunpw  10745  wunex2  10776  wuncval2  10785  eltskg  10788  eltsk2g  10789  tskpwss  10790  tskpw  10791  inar1  10813  grupw  10833  grothpw  10864  grothpwex  10865  axgroth6  10866  grothomex  10867  grothac  10868  axdc4uz  14022  hashpw  14472  hashbc  14489  ackbijnn  15861  incexclem  15869  rami  17049  ismre  17635  isacs  17696  isacs2  17698  acsfiel  17699  isacs1i  17702  mreacs  17703  isssc  17868  acsficl  18605  efmnd  18896  pmtrfval  19483  selvffval  22155  istopg  22917  istopon  22934  eltg  22980  tgdom  23001  ntrval  23060  nrmsep3  23379  iscmp  23412  cmpcov  23413  cmpsublem  23423  cmpsub  23424  tgcmp  23425  uncmp  23427  hauscmplem  23430  is1stc  23465  2ndc1stc  23475  llyi  23498  nllyi  23499  cldllycmp  23519  isfbas  23853  isfil  23871  filss  23877  fgval  23894  elfg  23895  isufil  23927  alexsublem  24068  alexsubb  24070  alexsubALTlem1  24071  alexsubALTlem2  24072  alexsubALTlem4  24074  alexsubALT  24075  restmetu  24599  bndth  25004  ovolicc2  25571  uhgreq12g  29097  uhgr0vb  29104  isupgr  29116  isumgr  29127  isuspgr  29184  isusgr  29185  isausgr  29196  lfuhgr1v0e  29286  nbuhgr2vtx1edgblem  29383  ex-pw  30458  iscref  33805  indv  33993  sigaval  34092  issiga  34093  isrnsiga  34094  issgon  34104  isldsys  34137  issros  34156  measval  34179  isrnmeas  34181  rankpwg  36151  neibastop1  36342  neibastop2lem  36343  neibastop2  36344  neibastop3  36345  neifg  36354  limsucncmpi  36428  bj-snglex  36956  bj-ismoore  37088  pibp19  37397  pibt2  37400  cover2g  37703  isnacs  42692  mrefg2  42695  aomclem8  43050  islssfg2  43060  lnr2i  43105  pwelg  43550  fsovd  43998  fsovcnvlem  44003  dssmapfvd  44007  clsk1independent  44036  ntrneibex  44063  mnuop123d  44258  stoweidlem50  46006  stoweidlem57  46013  issal  46270  omessle  46454  grtri  47845  vsetrec  48934  elpglem3  48944  pgindnf  48947