Theorem pweq 4161

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 3627	. . 3 |- ( A = B -> ( x C_ A <-> x C_ B ) )
2	1	abbidv 2741	. 2 |- ( A = B -> { x | x C_ A } = { x | x C_ B } )
3		df-pw 4160	. 2 |- ~P A = { x | x C_ A }
4		df-pw 4160	. 2 |- ~P B = { x | x C_ B }
5	2, 3, 4	3eqtr4g 2681	1 |- ( A = B -> ~P A = ~P B )

Syntax hints:   -> wi 4   = wceq 1483   {cab 2608   C_ wss 3574   ~Pcpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  pweqi  4162  pweqd  4163  axpweq  4842  pwex  4848  pwexg  4850  pwssun  5020  knatar  6607  pwdom  8112  canth2g  8114  pwfi  8261  fival  8318  marypha1lem  8339  marypha1  8340  wdompwdom  8483  canthwdom  8484  r1sucg  8632  ranklim  8707  r1pwALT  8709  isacn  8867  dfac12r  8968  dfac12k  8969  pwsdompw  9026  ackbij1lem5  9046  ackbij1lem8  9049  ackbij1lem14  9055  r1om  9066  fictb  9067  isfin1a  9114  isfin2  9116  isfin3  9118  isfin3ds  9151  isf33lem  9188  domtriomlem  9264  ttukeylem1  9331  elgch  9444  wunpw  9529  wunex2  9560  wuncval2  9569  eltskg  9572  eltsk2g  9573  tskpwss  9574  tskpw  9575  inar1  9597  grupw  9617  grothpw  9648  grothpwex  9649  axgroth6  9650  grothomex  9651  grothac  9652  axdc4uz  12783  hashpw  13223  hashbc  13237  ackbijnn  14560  incexclem  14568  rami  15719  ismre  16250  isacs  16312  isacs2  16314  acsfiel  16315  isacs1i  16318  mreacs  16319  isssc  16480  acsficl  17171  pmtrfval  17870  istopg  20700  istopon  20717  eltg  20761  tgdom  20782  ntrval  20840  nrmsep3  21159  iscmp  21191  cmpcov  21192  cmpsublem  21202  cmpsub  21203  tgcmp  21204  uncmp  21206  hauscmplem  21209  is1stc  21244  2ndc1stc  21254  llyi  21277  nllyi  21278  cldllycmp  21298  isfbas  21633  isfil  21651  filss  21657  fgval  21674  elfg  21675  isufil  21707  alexsublem  21848  alexsubb  21850  alexsubALTlem1  21851  alexsubALTlem2  21852  alexsubALTlem4  21854  alexsubALT  21855  restmetu  22375  bndth  22757  ovolicc2  23290  uhgreq12g  25960  uhgr0vb  25967  isupgr  25979  isumgr  25990  isuspgr  26047  isusgr  26048  isausgr  26059  lfuhgr1v0e  26146  usgrexmpl  26155  nbuhgr2vtx1edgblem  26247  ex-pw  27286  iscref  29911  indv  30074  sigaval  30173  issiga  30174  isrnsigaOLD  30175  isrnsiga  30176  issgon  30186  isldsys  30219  issros  30238  measval  30261  isrnmeas  30263  rankpwg  32276  neibastop1  32354  neibastop2lem  32355  neibastop2  32356  neibastop3  32357  neifg  32366  limsucncmpi  32444  bj-snglex  32961  bj-ismoore  33059  cover2g  33509  isnacs  37267  mrefg2  37270  aomclem8  37631  islssfg2  37641  lnr2i  37686  pwelg  37865  fsovd  38302  fsovcnvlem  38307  dssmapfvd  38311  clsk1independent  38344  ntrneibex  38371  stoweidlem50  40267  stoweidlem57  40274  issal  40534  omessle  40712  vsetrec  42446  elpglem3  42456