Theorem pweq 4111

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 3590	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵))
2	1	abbidv 2728	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 ⊆ 𝐴} = {𝑥 ∣ 𝑥 ⊆ 𝐵})
3		df-pw 4110	. 2 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}
4		df-pw 4110	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
5	2, 3, 4	3eqtr4g 2669	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1475  {cab 2596   ⊆ wss 3540  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  pweqi  4112  pweqd  4113  axpweq  4768  pwex  4774  pwexg  4776  pwssun  4944  knatar  6507  pwdom  7997  canth2g  7999  pwfi  8144  fival  8201  marypha1lem  8222  marypha1  8223  wdompwdom  8366  canthwdom  8367  r1sucg  8515  ranklim  8590  r1pwALT  8592  isacn  8750  dfac12r  8851  dfac12k  8852  pwsdompw  8909  ackbij1lem5  8929  ackbij1lem8  8932  ackbij1lem14  8938  r1om  8949  fictb  8950  isfin1a  8997  isfin2  8999  isfin3  9001  isfin3ds  9034  isf33lem  9071  domtriomlem  9147  ttukeylem1  9214  elgch  9323  wunpw  9408  wunex2  9439  wuncval2  9448  eltskg  9451  eltsk2g  9452  tskpwss  9453  tskpw  9454  inar1  9476  grupw  9496  grothpw  9527  grothpwex  9528  axgroth6  9529  grothomex  9530  grothac  9531  axdc4uz  12645  hashpw  13083  hashbc  13094  ackbijnn  14399  incexclem  14407  rami  15557  ismre  16073  isacs  16135  isacs2  16137  acsfiel  16138  isacs1i  16141  mreacs  16142  isssc  16303  acsficl  16994  pmtrfval  17693  istopg  20525  istopon  20540  eltg  20572  tgdom  20593  ntrval  20650  nrmsep3  20969  iscmp  21001  cmpcov  21002  cmpsublem  21012  cmpsub  21013  tgcmp  21014  uncmp  21016  hauscmplem  21019  is1stc  21054  2ndc1stc  21064  llyi  21087  nllyi  21088  cldllycmp  21108  isfbas  21443  isfil  21461  filss  21467  fgval  21484  elfg  21485  isufil  21517  alexsublem  21658  alexsubb  21660  alexsubALTlem1  21661  alexsubALTlem2  21662  alexsubALTlem4  21664  alexsubALT  21665  restmetu  22185  bndth  22565  ovolicc2  23097  uhgreq12g  25731  uhgr0vb  25738  isupgr  25751  isumgr  25761  isuhgra  25827  isushgra  25830  uhgrac  25834  uhgraeq12d  25836  isausgra  25883  usgraeq12d  25891  ex-pw  26678  iscref  29239  indv  29402  sigaval  29500  issiga  29501  isrnsigaOLD  29502  isrnsiga  29503  issgon  29513  isldsys  29546  issros  29565  measval  29588  isrnmeas  29590  rankpwg  31446  neibastop1  31524  neibastop2lem  31525  neibastop2  31526  neibastop3  31527  neifg  31536  limsucncmpi  31614  bj-snglex  32154  cover2g  32679  isnacs  36285  mrefg2  36288  aomclem8  36649  islssfg2  36659  lnr2i  36705  pwelg  36884  fsovd  37322  fsovcnvlem  37327  dssmapfvd  37331  clsk1independent  37364  ntrneibex  37391  stoweidlem50  38943  stoweidlem57  38950  issal  39210  omessle  39388  uhgruhgra  40375  uhgrauhgr  40376  isuspgr  40382  isusgr  40383  isausgr  40394  lfuhgr1v0e  40480  usgrexmpl  40487  nbuhgr2vtx1edgblem  40573  vsetrec  42245  elpglem3  42255