Theorem pweq 4569

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 3994	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4568	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3995	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4568	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3953	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1560  𝒫 cpw 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-pw 4557

This theorem is referenced by:  pweqi  4571  pweqd  4572  axpweq  5307  pwexg  5335  pwssun  5539  knatar  7341  pwdom  9101  canth2g  9103  pwfi  9263  fival  9358  marypha1lem  9379  marypha1  9380  wdompwdom  9526  canthwdom  9527  r1sucg  9727  ranklim  9802  r1pwALT  9804  isacn  10000  dfac12r  10103  dfac12k  10104  pwsdompw  10159  ackbij1lem8  10182  ackbij1lem14  10188  r1om  10199  fictb  10200  isfin1a  10249  isfin2  10251  isfin3  10253  isfin3ds  10286  isf33lem  10323  domtriomlem  10399  ttukeylem1  10466  elgch  10580  wunpw  10665  wunex2  10696  wuncval2  10705  eltskg  10708  eltsk2g  10709  tskpwss  10710  tskpw  10711  inar1  10733  grupw  10753  grothpw  10784  grothpwex  10785  axgroth6  10786  grothomex  10787  grothac  10788  indv  12197  axdc4uz  13997  hashpw  14449  hashbc  14466  ackbijnn  15858  incexclem  15866  rami  17051  ismre  17618  isacs  17683  isacs2  17685  acsfiel  17686  isacs1i  17689  mreacs  17690  isssc  17853  acsficl  18579  efmnd  18904  pmtrfval  19490  selvffval  22171  istopg  22955  istopon  22972  eltg  23017  tgdom  23038  ntrval  23096  nrmsep3  23415  iscmp  23448  cmpcov  23449  cmpsublem  23459  cmpsub  23460  tgcmp  23461  uncmp  23463  hauscmplem  23466  is1stc  23501  2ndc1stc  23511  llyi  23534  nllyi  23535  cldllycmp  23555  isfbas  23889  isfil  23907  filss  23913  fgval  23930  elfg  23931  isufil  23963  alexsublem  24104  alexsubb  24106  alexsubALTlem1  24107  alexsubALTlem2  24108  alexsubALTlem4  24110  alexsubALT  24111  restmetu  24630  bndth  25020  ovolicc2  25584  uhgreq12g  29266  uhgr0vb  29273  isupgr  29285  isumgr  29296  isuspgr  29353  isusgr  29354  isausgr  29365  lfuhgr1v0e  29455  nbuhgr2vtx1edgblem  29552  ex-pw  30631  esplyval  33859  iscref  34141  sigaval  34408  issiga  34409  isrnsiga  34410  issgon  34420  isldsys  34453  issros  34472  measval  34495  isrnmeas  34497  rankpwg  36519  neibastop1  36719  neibastop2lem  36720  neibastop2  36721  neibastop3  36722  neifg  36731  limsucncmpi  36805  bj-snglex  37458  bj-ismoore  37595  pibp19  37908  pibt2  37911  cover2g  38215  isnacs  43285  mrefg2  43288  aomclem8  43638  islssfg2  43648  lnr2i  43693  pwelg  44136  fsovd  44584  fsovcnvlem  44589  dssmapfvd  44593  clsk1independent  44622  ntrneibex  44649  mnuop123d  44838  stoweidlem50  46624  stoweidlem57  46631  issal  46888  omessle  47072  grtri  48562  vsetrec  50324  elpglem3  50334  pgindnf  50337