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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-pw 4559

This theorem is used by:  pweqi  4573  pweqd  4574  axpweq  5315  pwexg  5343  pwssun  5547  knatar  7361  pwdom  9128  canth2g  9130  pwfi  9289  fival  9383  marypha1lem  9404  marypha1  9405  wdompwdom  9551  canthwdom  9552  r1sucg  9752  ranklim  9827  r1pwALT  9829  isacn  10048  dfac12r  10150  dfac12k  10151  pwsdompw  10206  ackbij1lem8  10229  ackbij1lem14  10235  r1om  10246  fictb  10247  isfin1a  10295  isfin2  10297  isfin3  10299  isfin3ds  10332  isf33lem  10369  domtriomlem  10445  ttukeylem1  10512  elgch  10632  wunpw  10717  wunex2  10748  wuncval2  10757  eltskg  10760  eltsk2g  10761  tskpwss  10762  tskpw  10763  inar1  10785  grupw  10805  grothpw  10836  grothpwex  10837  axgroth6  10838  grothomex  10839  grothac  10840  indv  12245  axdc4uz  14049  hashpw  14502  hashbc  14519  ackbijnn  15918  incexclem  15926  rami  17108  ismre  17675  isacs  17740  isacs2  17742  acsfiel  17743  isacs1i  17746  mreacs  17747  isssc  17910  acsficl  18636  efmnd  18980  pmtrfval  19578  selvffval  22335  istopg  23121  istopon  23138  eltg  23183  tgdom  23204  ntrval  23262  nrmsep3  23581  iscmp  23614  cmpcov  23615  cmpsublem  23625  cmpsub  23626  tgcmp  23627  uncmp  23629  hauscmplem  23632  is1stc  23667  2ndc1stc  23677  llyi  23701  nllyi  23702  cldllycmp  23722  isfbas  24056  isfil  24074  filss  24080  fgval  24097  elfg  24098  isufil  24130  alexsublem  24271  alexsubb  24273  alexsubALTlem1  24274  alexsubALTlem2  24275  alexsubALTlem4  24277  alexsubALT  24278  restmetu  24797  bndth  25187  ovolicc2  25751  uhgreq12g  29523  uhgr0vb  29530  isupgr  29542  isumgr  29553  isuspgr  29613  isusgr  29614  isausgr  29625  lfuhgr1v0e  29715  nbuhgr2vtx1edgblem  29812  ex-pw  30910  esplyval  34073  iscref  34355  sigaval  34622  issiga  34623  isrnsiga  34624  issgon  34634  isldsys  34668  issros  34687  measval  34710  isrnmeas  34712  rankpwg  36750  neibastop1  36979  neibastop2lem  36980  neibastop2  36981  neibastop3  36982  neifg  36991  limsucncmpi  37065  bj-snglex  37718  bj-ismoore  37856  pibp19  38169  pibt2  38172  cover2g  38467  isnacs  43550  mrefg2  43553  aomclem8  43903  islssfg2  43913  lnr2i  43958  pwelg  44401  fsovd  44849  fsovcnvlem  44854  dssmapfvd  44858  clsk1independent  44887  ntrneibex  44914  mnuop123d  45087  stoweidlem50  46879  stoweidlem57  46886  issal  47143  omessle  47327  grtri  48857  vsetrec  50630  elpglem3  50640  pgindnf  50643