Theorem pweq 4578

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 3996	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4577	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3997	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4577	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3955	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  𝒫 cpw 4564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-pw 4566

This theorem is used by:  pweqi  4580  pweqd  4581  axpweq  5323  pwexg  5351  pwssun  5555  knatar  7366  pwdom  9124  canth2g  9126  pwfi  9285  fival  9379  marypha1lem  9400  marypha1  9401  wdompwdom  9547  canthwdom  9548  r1sucg  9748  ranklim  9823  r1pwALT  9825  isacn  10044  dfac12r  10146  dfac12k  10147  pwsdompw  10202  ackbij1lem8  10225  ackbij1lem14  10231  r1om  10242  fictb  10243  isfin1a  10291  isfin2  10293  isfin3  10295  isfin3ds  10328  isf33lem  10365  domtriomlem  10441  ttukeylem1  10508  elgch  10622  wunpw  10707  wunex2  10738  wuncval2  10747  eltskg  10750  eltsk2g  10751  tskpwss  10752  tskpw  10753  inar1  10775  grupw  10795  grothpw  10826  grothpwex  10827  axgroth6  10828  grothomex  10829  grothac  10830  indv  12235  axdc4uz  14038  hashpw  14491  hashbc  14508  ackbijnn  15905  incexclem  15913  rami  17097  ismre  17664  isacs  17729  isacs2  17731  acsfiel  17732  isacs1i  17735  mreacs  17736  isssc  17899  acsficl  18625  efmnd  18966  pmtrfval  19564  selvffval  22319  istopg  23102  istopon  23119  eltg  23164  tgdom  23185  ntrval  23243  nrmsep3  23562  iscmp  23595  cmpcov  23596  cmpsublem  23606  cmpsub  23607  tgcmp  23608  uncmp  23610  hauscmplem  23613  is1stc  23648  2ndc1stc  23658  llyi  23682  nllyi  23683  cldllycmp  23703  isfbas  24037  isfil  24055  filss  24061  fgval  24078  elfg  24079  isufil  24111  alexsublem  24252  alexsubb  24254  alexsubALTlem1  24255  alexsubALTlem2  24256  alexsubALTlem4  24258  alexsubALT  24259  restmetu  24778  bndth  25168  ovolicc2  25732  uhgreq12g  29470  uhgr0vb  29477  isupgr  29489  isumgr  29500  isuspgr  29560  isusgr  29561  isausgr  29572  lfuhgr1v0e  29662  nbuhgr2vtx1edgblem  29759  ex-pw  30851  esplyval  34016  iscref  34298  sigaval  34565  issiga  34566  isrnsiga  34567  issgon  34577  isldsys  34611  issros  34630  measval  34653  isrnmeas  34655  rankpwg  36698  neibastop1  36927  neibastop2lem  36928  neibastop2  36929  neibastop3  36930  neifg  36939  limsucncmpi  37013  bj-snglex  37666  bj-ismoore  37804  pibp19  38117  pibt2  38120  cover2g  38425  isnacs  43493  mrefg2  43496  aomclem8  43846  islssfg2  43856  lnr2i  43901  pwelg  44344  fsovd  44792  fsovcnvlem  44797  dssmapfvd  44801  clsk1independent  44830  ntrneibex  44857  mnuop123d  45030  stoweidlem50  46822  stoweidlem57  46829  issal  47086  omessle  47270  grtri  48763  vsetrec  50538  elpglem3  50548  pgindnf  50551