Theorem pweq 3858

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

Assertion

Ref	Expression
pweq	|- ( A = B -> ~P A = ~P B )

Proof of Theorem pweq

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq2 3373	. . 3 |- ( A = B -> ( x C_ A <-> x C_ B ) )
2	1	abbidv 2552	. 2 |- ( A = B -> { x | x C_ A } = { x | x C_ B } )
3		df-pw 3857	. 2 |- ~P A = { x | x C_ A }
4		df-pw 3857	. 2 |- ~P B = { x | x C_ B }
5	2, 3, 4	3eqtr4g 2495	1 |- ( A = B -> ~P A = ~P B )

Syntax hints:   -> wi 4   = wceq 1369   {cab 2424   C_ wss 3323   ~Pcpw 3855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337  df-pw 3857

This theorem is referenced by:  pweqi  3859  pweqd  3860  axpweq  4464  pwex  4470  pwexg  4471  pwssun  4622  knatar  6043  pwdom  7455  canth2g  7457  pwfi  7598  fival  7654  marypha1lem  7675  marypha1  7676  wdompwdom  7785  canthwdom  7786  r1sucg  7968  ranklim  8043  r1pwOLD  8045  isacn  8206  dfac12r  8307  dfac12k  8308  pwsdompw  8365  ackbij1lem5  8385  ackbij1lem8  8388  ackbij1lem14  8394  r1om  8405  fictb  8406  isfin1a  8453  isfin2  8455  isfin3  8457  isfin3ds  8490  isf33lem  8527  domtriomlem  8603  ttukeylem1  8670  elgch  8781  wunpw  8866  wunex2  8897  wuncval2  8906  eltskg  8909  eltsk2g  8910  tskpwss  8911  tskpw  8912  inar1  8934  grupw  8954  grothpw  8985  grothpwex  8986  axgroth6  8987  grothomex  8988  grothac  8989  axdc4uz  11797  hashpw  12190  hashbc  12198  ackbijnn  13283  incexclem  13291  rami  14068  ismre  14520  isacs  14581  isacs2  14583  acsfiel  14584  isacs1i  14587  mreacs  14588  isssc  14725  acsficl  15333  pmtrfval  15947  istopg  18483  istopon  18505  eltg  18537  tgdom  18558  ntrval  18615  nrmsep3  18934  iscmp  18966  cmpcov  18967  cmpsublem  18977  cmpsub  18978  tgcmp  18979  uncmp  18981  hauscmplem  18984  bwthOLD  18989  is1stc  19020  2ndc1stc  19030  llyi  19053  nllyi  19054  cldllycmp  19074  isfbas  19377  isfil  19395  filss  19401  fgval  19418  elfg  19419  isufil  19451  alexsublem  19591  alexsubb  19593  alexsubALTlem1  19594  alexsubALTlem2  19595  alexsubALTlem4  19597  alexsubALT  19598  restmetu  20137  bndth  20505  ovolicc2  20980  isuhgra  23188  uhgraeq12d  23192  isausgra  23229  usgraeq12d  23235  ex-pw  23587  issubgo  23741  indv  26421  sigaval  26505  issiga  26506  isrnsigaOLD  26507  isrnsiga  26508  issgon  26518  measval  26564  isrnmeas  26566  rankpwg  28158  limsucncmpi  28243  neibastop1  28533  neibastop2lem  28534  neibastop2  28535  neibastop3  28536  neifg  28545  cover2g  28561  isnacs  28993  mrefg2  28996  aomclem8  29367  islssfg2  29377  lnr2i  29425  stoweidlem50  29798  stoweidlem57  29805  bj-snglex  32313