Theorem pweq 4298

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

Syntax hints:   → wi 4   = wceq 1630  {cab 2756   ⊆ wss 3721  𝒫 cpw 4295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-in 3728  df-ss 3735  df-pw 4297

This theorem is referenced by:  pweqi  4299  pweqd  4300  axpweq  4970  pwex  4976  pwexg  4978  pwssun  5153  knatar  6749  pwdom  8267  canth2g  8269  pwfi  8416  fival  8473  marypha1lem  8494  marypha1  8495  wdompwdom  8638  canthwdom  8639  r1sucg  8795  ranklim  8870  r1pwALT  8872  isacn  9066  dfac12r  9169  dfac12k  9170  pwsdompw  9227  ackbij1lem8  9250  ackbij1lem14  9256  r1om  9267  fictb  9268  isfin1a  9315  isfin2  9317  isfin3  9319  isfin3ds  9352  isf33lem  9389  domtriomlem  9465  ttukeylem1  9532  elgch  9645  wunpw  9730  wunex2  9761  wuncval2  9770  eltskg  9773  eltsk2g  9774  tskpwss  9775  tskpw  9776  inar1  9798  grupw  9818  grothpw  9849  grothpwex  9850  axgroth6  9851  grothomex  9852  grothac  9853  axdc4uz  12990  hashpw  13424  hashbc  13438  ackbijnn  14766  incexclem  14774  rami  15925  ismre  16457  isacs  16518  isacs2  16520  acsfiel  16521  isacs1i  16524  mreacs  16525  isssc  16686  acsficl  17378  pmtrfval  18076  istopg  20919  istopon  20936  eltg  20981  tgdom  21002  ntrval  21060  nrmsep3  21379  iscmp  21411  cmpcov  21412  cmpsublem  21422  cmpsub  21423  tgcmp  21424  uncmp  21426  hauscmplem  21429  is1stc  21464  2ndc1stc  21474  llyi  21497  nllyi  21498  cldllycmp  21518  isfbas  21852  isfil  21870  filss  21876  fgval  21893  elfg  21894  isufil  21926  alexsublem  22067  alexsubb  22069  alexsubALTlem1  22070  alexsubALTlem2  22071  alexsubALTlem4  22073  alexsubALT  22074  restmetu  22594  bndth  22976  ovolicc2  23509  uhgreq12g  26180  uhgr0vb  26187  isupgr  26199  isumgr  26210  isuspgr  26268  isusgr  26269  isausgr  26280  lfuhgr1v0e  26368  usgrexmpl  26377  nbuhgr2vtx1edgblem  26469  ex-pw  27622  iscref  30245  indv  30408  sigaval  30507  issiga  30508  isrnsigaOLD  30509  isrnsiga  30510  issgon  30520  isldsys  30553  issros  30572  measval  30595  isrnmeas  30597  rankpwg  32607  neibastop1  32685  neibastop2lem  32686  neibastop2  32687  neibastop3  32688  neifg  32697  limsucncmpi  32775  bj-snglex  33286  bj-ismoore  33384  cover2g  33834  isnacs  37786  mrefg2  37789  aomclem8  38150  islssfg2  38160  lnr2i  38205  pwelg  38384  fsovd  38821  fsovcnvlem  38826  dssmapfvd  38830  clsk1independent  38863  ntrneibex  38890  stoweidlem50  40778  stoweidlem57  40785  issal  41045  omessle  41226  vsetrec  42967  elpglem3  42977