Theorem pweq 4571

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 3989	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4570	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3990	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4570	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3948	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-pw 4559

This theorem is used by:  pweqi  4573  pweqd  4574  axpweq  5312  pwexg  5340  pwssun  5543  knatar  7367  pwdom  9148  canth2g  9150  pwfi  9310  fival  9404  marypha1lem  9425  marypha1  9426  wdompwdom  9572  canthwdom  9573  r1sucg  9776  rankpwg  9857  ranklim  9858  r1pwALT  9860  isacn  10123  dfac12r  10225  dfac12k  10226  pwsdompw  10281  ackbij1lem8  10304  ackbij1lem14  10310  hfom  10321  fictb  10322  isfin1a  10370  isfin2  10372  isfin3  10374  isfin3ds  10407  isf33lem  10444  domtriomlem  10520  ttukeylem1  10587  elgch  10707  wunpw  10792  wunex2  10823  wuncval2  10832  eltskg  10835  eltsk2g  10836  tskpwss  10837  tskpw  10838  inar1  10860  grupw  10880  grothpw  10911  grothpwex  10912  axgroth6  10913  grothomex  10914  grothac  10915  indv  12322  axdc4uz  14127  hashpw  14581  hashbc  14598  ackbijnn  15997  incexclem  16005  rami  17193  ismre  17760  isacs  17825  isacs2  17827  acsfiel  17828  isacs1i  17831  mreacs  17832  isssc  17995  acsficl  18721  efmnd  19066  pmtrfval  19664  selvffval  22427  istopg  23213  istopon  23230  eltg  23275  tgdom  23296  ntrval  23354  nrmsep3  23673  iscmp  23706  cmpcov  23707  cmpsublem  23717  cmpsub  23718  tgcmp  23719  uncmp  23721  hauscmplem  23724  is1stc  23759  2ndc1stc  23769  llyi  23793  nllyi  23794  cldllycmp  23814  isfbas  24148  isfil  24166  filss  24172  fgval  24189  elfg  24190  isufil  24222  alexsublem  24363  alexsubb  24365  alexsubALTlem1  24366  alexsubALTlem2  24367  alexsubALTlem4  24369  alexsubALT  24370  restmetu  24889  bndth  25279  ovolicc2  25843  uhgreq12g  29643  uhgr0vb  29650  isupgr  29662  isumgr  29673  isuspgr  29733  isusgr  29734  isausgr  29745  lfuhgr1v0e  29835  nbuhgr2vtx1edgblem  29932  ex-pw  31030  esplyval  34194  iscref  34476  sigaval  34743  issiga  34744  isrnsiga  34745  issgon  34755  isldsys  34789  issros  34808  measval  34831  isrnmeas  34833  neibastop1  37147  neibastop2lem  37148  neibastop2  37149  neibastop3  37150  neifg  37159  limsucncmpi  37233  bj-snglex  37886  bj-ismoore  38026  pibp19  38337  pibt2  38340  cover2g  38650  isnacs  43714  mrefg2  43717  aomclem8  44062  islssfg2  44072  lnr2i  44117  pwelg  44560  fsovd  45007  fsovcnvlem  45012  dssmapfvd  45016  clsk1independent  45045  ntrneibex  45072  mnuop123d  45245  stoweidlem50  47059  stoweidlem57  47066  issal  47323  omessle  47507  grtri  49037  vsetrec  50795  elpglem3  50805  pgindnf  50808