Theorem pweq 4159

Description: Equality theorem for power class. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
pweq	⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Proof of Theorem pweq

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq2 3625	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵))
2	1	abbidv 2740	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 ⊆ 𝐴} = {𝑥 ∣ 𝑥 ⊆ 𝐵})
3		df-pw 4158	. 2 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}
4		df-pw 4158	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
5	2, 3, 4	3eqtr4g 2680	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1482  {cab 2607   ⊆ wss 3572  𝒫 cpw 4156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3579  df-ss 3586  df-pw 4158

This theorem is referenced by:  pweqi  4160  pweqd  4161  axpweq  4840  pwex  4846  pwexg  4848  pwssun  5018  knatar  6604  pwdom  8109  canth2g  8111  pwfi  8258  fival  8315  marypha1lem  8336  marypha1  8337  wdompwdom  8480  canthwdom  8481  r1sucg  8629  ranklim  8704  r1pwALT  8706  isacn  8864  dfac12r  8965  dfac12k  8966  pwsdompw  9023  ackbij1lem5  9043  ackbij1lem8  9046  ackbij1lem14  9052  r1om  9063  fictb  9064  isfin1a  9111  isfin2  9113  isfin3  9115  isfin3ds  9148  isf33lem  9185  domtriomlem  9261  ttukeylem1  9328  elgch  9441  wunpw  9526  wunex2  9557  wuncval2  9566  eltskg  9569  eltsk2g  9570  tskpwss  9571  tskpw  9572  inar1  9594  grupw  9614  grothpw  9645  grothpwex  9646  axgroth6  9647  grothomex  9648  grothac  9649  axdc4uz  12778  hashpw  13218  hashbc  13232  ackbijnn  14554  incexclem  14562  rami  15713  ismre  16244  isacs  16306  isacs2  16308  acsfiel  16309  isacs1i  16312  mreacs  16313  isssc  16474  acsficl  17165  pmtrfval  17864  istopg  20694  istopon  20711  eltg  20755  tgdom  20776  ntrval  20834  nrmsep3  21153  iscmp  21185  cmpcov  21186  cmpsublem  21196  cmpsub  21197  tgcmp  21198  uncmp  21200  hauscmplem  21203  is1stc  21238  2ndc1stc  21248  llyi  21271  nllyi  21272  cldllycmp  21292  isfbas  21627  isfil  21645  filss  21651  fgval  21668  elfg  21669  isufil  21701  alexsublem  21842  alexsubb  21844  alexsubALTlem1  21845  alexsubALTlem2  21846  alexsubALTlem4  21848  alexsubALT  21849  restmetu  22369  bndth  22751  ovolicc2  23284  uhgreq12g  25954  uhgr0vb  25961  isupgr  25973  isumgr  25984  isuspgr  26041  isusgr  26042  isausgr  26053  lfuhgr1v0e  26140  usgrexmpl  26149  nbuhgr2vtx1edgblem  26241  ex-pw  27270  iscref  29896  indv  30059  sigaval  30158  issiga  30159  isrnsigaOLD  30160  isrnsiga  30161  issgon  30171  isldsys  30204  issros  30223  measval  30246  isrnmeas  30248  rankpwg  32260  neibastop1  32338  neibastop2lem  32339  neibastop2  32340  neibastop3  32341  neifg  32350  limsucncmpi  32428  bj-snglex  32945  bj-ismoore  33043  cover2g  33489  isnacs  37093  mrefg2  37096  aomclem8  37457  islssfg2  37467  lnr2i  37512  pwelg  37691  fsovd  38128  fsovcnvlem  38133  dssmapfvd  38137  clsk1independent  38170  ntrneibex  38197  stoweidlem50  40036  stoweidlem57  40043  issal  40303  omessle  40481  vsetrec  42217  elpglem3  42227