Theorem pweq 4570

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 3994	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4569	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3995	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4569	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3953	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-pw 4558

This theorem is referenced by:  pweqi  4572  pweqd  4573  axpweq  5298  pwexg  5325  pwssun  5524  knatar  7313  pwdom  9069  canth2g  9071  pwfi  9231  fival  9327  marypha1lem  9348  marypha1  9349  wdompwdom  9495  canthwdom  9496  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  axdc4uz  13919  hashpw  14371  hashbc  14388  ackbijnn  15763  incexclem  15771  rami  16955  ismre  17521  isacs  17586  isacs2  17588  acsfiel  17589  isacs1i  17592  mreacs  17593  isssc  17756  acsficl  18482  efmnd  18807  pmtrfval  19391  selvffval  22088  istopg  22851  istopon  22868  eltg  22913  tgdom  22934  ntrval  22992  nrmsep3  23311  iscmp  23344  cmpcov  23345  cmpsublem  23355  cmpsub  23356  tgcmp  23357  uncmp  23359  hauscmplem  23362  is1stc  23397  2ndc1stc  23407  llyi  23430  nllyi  23431  cldllycmp  23451  isfbas  23785  isfil  23803  filss  23809  fgval  23826  elfg  23827  isufil  23859  alexsublem  24000  alexsubb  24002  alexsubALTlem1  24003  alexsubALTlem2  24004  alexsubALTlem4  24006  alexsubALT  24007  restmetu  24526  bndth  24925  ovolicc2  25491  uhgreq12g  29150  uhgr0vb  29157  isupgr  29169  isumgr  29180  isuspgr  29237  isusgr  29238  isausgr  29249  lfuhgr1v0e  29339  nbuhgr2vtx1edgblem  29436  ex-pw  30516  indv  32942  esplyval  33739  iscref  34022  sigaval  34289  issiga  34290  isrnsiga  34291  issgon  34301  isldsys  34334  issros  34353  measval  34376  isrnmeas  34378  rankpwg  36385  neibastop1  36575  neibastop2lem  36576  neibastop2  36577  neibastop3  36578  neifg  36587  limsucncmpi  36661  bj-snglex  37221  bj-ismoore  37358  pibp19  37669  pibt2  37672  cover2g  37967  isnacs  43061  mrefg2  43064  aomclem8  43418  islssfg2  43428  lnr2i  43473  pwelg  43916  fsovd  44364  fsovcnvlem  44369  dssmapfvd  44373  clsk1independent  44402  ntrneibex  44429  mnuop123d  44618  stoweidlem50  46408  stoweidlem57  46415  issal  46672  omessle  46856  grtri  48300  vsetrec  50062  elpglem3  50072  pgindnf  50075