Theorem pweq 4555

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 3980	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4554	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3981	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4554	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3939	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-pw 4543

This theorem is referenced by:  pweqi  4557  pweqd  4558  axpweq  5292  pwexg  5320  pwssun  5523  knatar  7312  pwdom  9067  canth2g  9069  pwfi  9229  fival  9325  marypha1lem  9346  marypha1  9347  wdompwdom  9493  canthwdom  9494  r1sucg  9693  ranklim  9768  r1pwALT  9770  isacn  9966  dfac12r  10069  dfac12k  10070  pwsdompw  10125  ackbij1lem8  10148  ackbij1lem14  10154  r1om  10165  fictb  10166  isfin1a  10214  isfin2  10216  isfin3  10218  isfin3ds  10251  isf33lem  10288  domtriomlem  10364  ttukeylem1  10431  elgch  10545  wunpw  10630  wunex2  10661  wuncval2  10670  eltskg  10673  eltsk2g  10674  tskpwss  10675  tskpw  10676  inar1  10698  grupw  10718  grothpw  10749  grothpwex  10750  axgroth6  10751  grothomex  10752  grothac  10753  indv  12161  axdc4uz  13946  hashpw  14398  hashbc  14415  ackbijnn  15793  incexclem  15801  rami  16986  ismre  17552  isacs  17617  isacs2  17619  acsfiel  17620  isacs1i  17623  mreacs  17624  isssc  17787  acsficl  18513  efmnd  18838  pmtrfval  19425  selvffval  22099  istopg  22860  istopon  22877  eltg  22922  tgdom  22943  ntrval  23001  nrmsep3  23320  iscmp  23353  cmpcov  23354  cmpsublem  23364  cmpsub  23365  tgcmp  23366  uncmp  23368  hauscmplem  23371  is1stc  23406  2ndc1stc  23416  llyi  23439  nllyi  23440  cldllycmp  23460  isfbas  23794  isfil  23812  filss  23818  fgval  23835  elfg  23836  isufil  23868  alexsublem  24009  alexsubb  24011  alexsubALTlem1  24012  alexsubALTlem2  24013  alexsubALTlem4  24015  alexsubALT  24016  restmetu  24535  bndth  24925  ovolicc2  25489  uhgreq12g  29134  uhgr0vb  29141  isupgr  29153  isumgr  29164  isuspgr  29221  isusgr  29222  isausgr  29233  lfuhgr1v0e  29323  nbuhgr2vtx1edgblem  29420  ex-pw  30499  esplyval  33706  iscref  33988  sigaval  34255  issiga  34256  isrnsiga  34257  issgon  34267  isldsys  34300  issros  34319  measval  34342  isrnmeas  34344  rankpwg  36351  neibastop1  36541  neibastop2lem  36542  neibastop2  36543  neibastop3  36544  neifg  36553  limsucncmpi  36627  bj-snglex  37280  bj-ismoore  37417  pibp19  37730  pibt2  37733  cover2g  38037  isnacs  43136  mrefg2  43139  aomclem8  43489  islssfg2  43499  lnr2i  43544  pwelg  43987  fsovd  44435  fsovcnvlem  44440  dssmapfvd  44444  clsk1independent  44473  ntrneibex  44500  mnuop123d  44689  stoweidlem50  46478  stoweidlem57  46485  issal  46742  omessle  46926  grtri  48416  vsetrec  50178  elpglem3  50188  pgindnf  50191