Theorem pweq 4568

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 3992	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4567	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3993	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4567	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3951	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1541  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-pw 4556

This theorem is referenced by:  pweqi  4570  pweqd  4571  axpweq  5296  pwexg  5323  pwssun  5516  knatar  7303  pwdom  9057  canth2g  9059  pwfi  9219  fival  9315  marypha1lem  9336  marypha1  9337  wdompwdom  9483  canthwdom  9484  r1sucg  9681  ranklim  9756  r1pwALT  9758  isacn  9954  dfac12r  10057  dfac12k  10058  pwsdompw  10113  ackbij1lem8  10136  ackbij1lem14  10142  r1om  10153  fictb  10154  isfin1a  10202  isfin2  10204  isfin3  10206  isfin3ds  10239  isf33lem  10276  domtriomlem  10352  ttukeylem1  10419  elgch  10533  wunpw  10618  wunex2  10649  wuncval2  10658  eltskg  10661  eltsk2g  10662  tskpwss  10663  tskpw  10664  inar1  10686  grupw  10706  grothpw  10737  grothpwex  10738  axgroth6  10739  grothomex  10740  grothac  10741  axdc4uz  13907  hashpw  14359  hashbc  14376  ackbijnn  15751  incexclem  15759  rami  16943  ismre  17509  isacs  17574  isacs2  17576  acsfiel  17577  isacs1i  17580  mreacs  17581  isssc  17744  acsficl  18470  efmnd  18795  pmtrfval  19379  selvffval  22076  istopg  22839  istopon  22856  eltg  22901  tgdom  22922  ntrval  22980  nrmsep3  23299  iscmp  23332  cmpcov  23333  cmpsublem  23343  cmpsub  23344  tgcmp  23345  uncmp  23347  hauscmplem  23350  is1stc  23385  2ndc1stc  23395  llyi  23418  nllyi  23419  cldllycmp  23439  isfbas  23773  isfil  23791  filss  23797  fgval  23814  elfg  23815  isufil  23847  alexsublem  23988  alexsubb  23990  alexsubALTlem1  23991  alexsubALTlem2  23992  alexsubALTlem4  23994  alexsubALT  23995  restmetu  24514  bndth  24913  ovolicc2  25479  uhgreq12g  29138  uhgr0vb  29145  isupgr  29157  isumgr  29168  isuspgr  29225  isusgr  29226  isausgr  29237  lfuhgr1v0e  29327  nbuhgr2vtx1edgblem  29424  ex-pw  30504  indv  32931  esplyval  33720  iscref  34001  sigaval  34268  issiga  34269  isrnsiga  34270  issgon  34280  isldsys  34313  issros  34332  measval  34355  isrnmeas  34357  rankpwg  36363  neibastop1  36553  neibastop2lem  36554  neibastop2  36555  neibastop3  36556  neifg  36565  limsucncmpi  36639  bj-snglex  37174  bj-ismoore  37310  pibp19  37619  pibt2  37622  cover2g  37917  isnacs  42946  mrefg2  42949  aomclem8  43303  islssfg2  43313  lnr2i  43358  pwelg  43801  fsovd  44249  fsovcnvlem  44254  dssmapfvd  44258  clsk1independent  44287  ntrneibex  44314  mnuop123d  44503  stoweidlem50  46294  stoweidlem57  46301  issal  46558  omessle  46742  grtri  48186  vsetrec  49948  elpglem3  49958  pgindnf  49961