Theorem pweq 4580

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 4008	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4579	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 4009	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4579	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3967	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1540  𝒫 cpw 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-pw 4568

This theorem is referenced by:  pweqi  4582  pweqd  4583  axpweq  5309  pwexg  5336  pwssun  5533  knatar  7335  pwdom  9099  canth2g  9101  pwfi  9275  fival  9370  marypha1lem  9391  marypha1  9392  wdompwdom  9538  canthwdom  9539  r1sucg  9729  ranklim  9804  r1pwALT  9806  isacn  10004  dfac12r  10107  dfac12k  10108  pwsdompw  10163  ackbij1lem8  10186  ackbij1lem14  10192  r1om  10203  fictb  10204  isfin1a  10252  isfin2  10254  isfin3  10256  isfin3ds  10289  isf33lem  10326  domtriomlem  10402  ttukeylem1  10469  elgch  10582  wunpw  10667  wunex2  10698  wuncval2  10707  eltskg  10710  eltsk2g  10711  tskpwss  10712  tskpw  10713  inar1  10735  grupw  10755  grothpw  10786  grothpwex  10787  axgroth6  10788  grothomex  10789  grothac  10790  axdc4uz  13956  hashpw  14408  hashbc  14425  ackbijnn  15801  incexclem  15809  rami  16993  ismre  17558  isacs  17619  isacs2  17621  acsfiel  17622  isacs1i  17625  mreacs  17626  isssc  17789  acsficl  18513  efmnd  18804  pmtrfval  19387  selvffval  22027  istopg  22789  istopon  22806  eltg  22851  tgdom  22872  ntrval  22930  nrmsep3  23249  iscmp  23282  cmpcov  23283  cmpsublem  23293  cmpsub  23294  tgcmp  23295  uncmp  23297  hauscmplem  23300  is1stc  23335  2ndc1stc  23345  llyi  23368  nllyi  23369  cldllycmp  23389  isfbas  23723  isfil  23741  filss  23747  fgval  23764  elfg  23765  isufil  23797  alexsublem  23938  alexsubb  23940  alexsubALTlem1  23941  alexsubALTlem2  23942  alexsubALTlem4  23944  alexsubALT  23945  restmetu  24465  bndth  24864  ovolicc2  25430  uhgreq12g  28999  uhgr0vb  29006  isupgr  29018  isumgr  29029  isuspgr  29086  isusgr  29087  isausgr  29098  lfuhgr1v0e  29188  nbuhgr2vtx1edgblem  29285  ex-pw  30365  indv  32782  iscref  33841  sigaval  34108  issiga  34109  isrnsiga  34110  issgon  34120  isldsys  34153  issros  34172  measval  34195  isrnmeas  34197  rankpwg  36164  neibastop1  36354  neibastop2lem  36355  neibastop2  36356  neibastop3  36357  neifg  36366  limsucncmpi  36440  bj-snglex  36968  bj-ismoore  37100  pibp19  37409  pibt2  37412  cover2g  37717  isnacs  42699  mrefg2  42702  aomclem8  43057  islssfg2  43067  lnr2i  43112  pwelg  43556  fsovd  44004  fsovcnvlem  44009  dssmapfvd  44013  clsk1independent  44042  ntrneibex  44069  mnuop123d  44258  stoweidlem50  46055  stoweidlem57  46062  issal  46319  omessle  46503  grtri  47943  vsetrec  49696  elpglem3  49706  pgindnf  49709