Theorem pweq 3966

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 3466	. . 3 |- ( A = B -> ( x C_ A <-> x C_ B ) )
2	1	abbidv 2580	. 2 |- ( A = B -> { x | x C_ A } = { x | x C_ B } )
3		df-pw 3965	. 2 |- ~P A = { x | x C_ A }
4		df-pw 3965	. 2 |- ~P B = { x | x C_ B }
5	2, 3, 4	3eqtr4g 2521	1 |- ( A = B -> ~P A = ~P B )

Syntax hints:   -> wi 4   = wceq 1455   {cab 2448   C_ wss 3416   ~Pcpw 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430  df-pw 3965

This theorem is referenced by:  pweqi  3967  pweqd  3968  axpweq  4597  pwex  4603  pwexg  4604  pwssun  4762  knatar  6278  pwdom  7755  canth2g  7757  pwfi  7900  fival  7957  marypha1lem  7978  marypha1  7979  wdompwdom  8124  canthwdom  8125  r1sucg  8271  ranklim  8346  r1pwALT  8348  isacn  8506  dfac12r  8607  dfac12k  8608  pwsdompw  8665  ackbij1lem5  8685  ackbij1lem8  8688  ackbij1lem14  8694  r1om  8705  fictb  8706  isfin1a  8753  isfin2  8755  isfin3  8757  isfin3ds  8790  isf33lem  8827  domtriomlem  8903  ttukeylem1  8970  elgch  9078  wunpw  9163  wunex2  9194  wuncval2  9203  eltskg  9206  eltsk2g  9207  tskpwss  9208  tskpw  9209  inar1  9231  grupw  9251  grothpw  9282  grothpwex  9283  axgroth6  9284  grothomex  9285  grothac  9286  axdc4uz  12234  hashpw  12647  hashbc  12655  ackbijnn  13941  incexclem  13949  rami  15027  ismre  15551  isacs  15612  isacs2  15614  acsfiel  15615  isacs1i  15618  mreacs  15619  isssc  15780  acsficl  16472  pmtrfval  17146  istopg  19980  istopon  19995  eltg  20027  tgdom  20049  ntrval  20106  nrmsep3  20426  iscmp  20458  cmpcov  20459  cmpsublem  20469  cmpsub  20470  tgcmp  20471  uncmp  20473  hauscmplem  20476  is1stc  20511  2ndc1stc  20521  llyi  20544  nllyi  20545  cldllycmp  20565  isfbas  20899  isfil  20917  filss  20923  fgval  20940  elfg  20941  isufil  20973  alexsublem  21114  alexsubb  21116  alexsubALTlem1  21117  alexsubALTlem2  21118  alexsubALTlem4  21120  alexsubALT  21121  restmetu  21640  bndth  22041  ovolicc2  22531  isuhgra  25081  isushgra  25084  uhgrac  25088  uhgraeq12d  25090  isausgra  25137  usgraeq12d  25145  ex-pw  25935  issubgo  26087  iscref  28722  indv  28885  sigaval  28983  issiga  28984  isrnsigaOLD  28985  isrnsiga  28986  issgon  28996  isldsys  29029  issros  29048  measval  29071  isrnmeas  29073  rankpwg  30986  neibastop1  31065  neibastop2lem  31066  neibastop2  31067  neibastop3  31068  neifg  31077  limsucncmpi  31155  bj-snglex  31613  cover2g  32087  isnacs  35592  mrefg2  35595  aomclem8  35965  islssfg2  35975  lnr2i  36021  pwelg  36210  stoweidlem50  38012  stoweidlem57  38019  issal  38276  omessle  38427  uhgreq12g  39298  uhgruhgra  39303  uhgrauhgr  39304  uhgr0vb  39308  isupgr  39319  isumgr  39328  isuspgr  39383  isusgr  39384  isausgr  39395  usgr1vr  39475  usgrexmpl  39481  nbuhgr2vtx1edgblem  39565  uhgeq12gALTV  40051  uhguhgra  40053  uhgrauhg  40054  uhg0v  40058  isfusgra  40105