Theorem pweq 4636

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 4067	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4635	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 4068	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4635	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 4026	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1537  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-pw 4624

This theorem is referenced by:  pweqi  4638  pweqd  4639  axpweq  5369  pwexg  5396  pwssun  5590  knatar  7393  pwdom  9195  canth2g  9197  pwfi  9385  pwfiOLD  9417  fival  9481  marypha1lem  9502  marypha1  9503  wdompwdom  9647  canthwdom  9648  r1sucg  9838  ranklim  9913  r1pwALT  9915  isacn  10113  dfac12r  10216  dfac12k  10217  pwsdompw  10272  ackbij1lem8  10295  ackbij1lem14  10301  r1om  10312  fictb  10313  isfin1a  10361  isfin2  10363  isfin3  10365  isfin3ds  10398  isf33lem  10435  domtriomlem  10511  ttukeylem1  10578  elgch  10691  wunpw  10776  wunex2  10807  wuncval2  10816  eltskg  10819  eltsk2g  10820  tskpwss  10821  tskpw  10822  inar1  10844  grupw  10864  grothpw  10895  grothpwex  10896  axgroth6  10897  grothomex  10898  grothac  10899  axdc4uz  14035  hashpw  14485  hashbc  14502  ackbijnn  15876  incexclem  15884  rami  17062  ismre  17648  isacs  17709  isacs2  17711  acsfiel  17712  isacs1i  17715  mreacs  17716  isssc  17881  acsficl  18617  efmnd  18905  pmtrfval  19492  selvffval  22160  istopg  22922  istopon  22939  eltg  22985  tgdom  23006  ntrval  23065  nrmsep3  23384  iscmp  23417  cmpcov  23418  cmpsublem  23428  cmpsub  23429  tgcmp  23430  uncmp  23432  hauscmplem  23435  is1stc  23470  2ndc1stc  23480  llyi  23503  nllyi  23504  cldllycmp  23524  isfbas  23858  isfil  23876  filss  23882  fgval  23899  elfg  23900  isufil  23932  alexsublem  24073  alexsubb  24075  alexsubALTlem1  24076  alexsubALTlem2  24077  alexsubALTlem4  24079  alexsubALT  24080  restmetu  24604  bndth  25009  ovolicc2  25576  uhgreq12g  29100  uhgr0vb  29107  isupgr  29119  isumgr  29130  isuspgr  29187  isusgr  29188  isausgr  29199  lfuhgr1v0e  29289  nbuhgr2vtx1edgblem  29386  ex-pw  30461  iscref  33790  indv  33976  sigaval  34075  issiga  34076  isrnsiga  34077  issgon  34087  isldsys  34120  issros  34139  measval  34162  isrnmeas  34164  rankpwg  36133  neibastop1  36325  neibastop2lem  36326  neibastop2  36327  neibastop3  36328  neifg  36337  limsucncmpi  36411  bj-snglex  36939  bj-ismoore  37071  pibp19  37380  pibt2  37383  cover2g  37676  isnacs  42660  mrefg2  42663  aomclem8  43018  islssfg2  43028  lnr2i  43073  pwelg  43522  fsovd  43970  fsovcnvlem  43975  dssmapfvd  43979  clsk1independent  44008  ntrneibex  44035  mnuop123d  44231  stoweidlem50  45971  stoweidlem57  45978  issal  46235  omessle  46419  grtri  47791  vsetrec  48795  elpglem3  48805  pgindnf  48808