Theorem difeq2 3468

Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
difeq2	|- ( A = B -> ( C \ A ) = ( C \ B ) )

Proof of Theorem difeq2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2504	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	notbid 294	. . 3 |- ( A = B -> ( -. x e. A <-> -. x e. B ) )
3	2	rabbidv 2964	. 2 |- ( A = B -> { x e. C | -. x e. A } = { x e. C | -. x e. B } )
4		dfdif2 3337	. 2 |- ( C \ A ) = { x e. C | -. x e. A }
5		dfdif2 3337	. 2 |- ( C \ B ) = { x e. C | -. x e. B }
6	3, 4, 5	3eqtr4g 2500	1 |- ( A = B -> ( C \ A ) = ( C \ B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1369   e. wcel 1756   {crab 2719   \ cdif 3325

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 2423

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 2430  df-cleq 2436  df-clel 2439  df-ral 2720  df-rab 2724  df-dif 3331

This theorem is referenced by:  difeq12  3469  difeq2i  3471  difeq2d  3474  ssdifeq0  3761  sorpsscmpl  6371  2oconcl  6943  oev  6954  sbthlem2  7422  sbth  7431  infdiffi  7863  fin1ai  8462  fin23lem7  8485  fin23lem11  8486  compsscnv  8540  isf34lem1  8541  compss  8545  isf34lem4  8546  fin1a2lem7  8575  pwfseqlem4a  8828  pwfseqlem4  8829  efgmval  16209  efgi  16216  frgpuptinv  16268  gsumcllem  16386  gsumcllemOLD  16387  gsumzaddlem  16408  gsumzaddlemOLD  16410  fctop  18608  cctop  18610  iscld  18631  clsval2  18654  opncldf1  18688  opncldf2  18689  opncldf3  18690  indiscld  18695  mretopd  18696  restcld  18776  lecldbas  18823  pnrmopn  18947  hauscmplem  19009  elpt  19145  elptr  19146  ptbasfi  19154  cfinfil  19466  csdfil  19467  ufilss  19478  filufint  19493  cfinufil  19501  ufinffr  19502  ufilen  19503  prdsxmslem2  20104  lebnumlem1  20533  bcth3  20842  ismbl  21009  disjdifprg  25919  0elsiga  26557  prsiga  26574  sigaclci  26575  difelsiga  26576  ballotlemfval  26872  ballotlemgval  26906  kur14lem1  27094  symdifeq1  27851  frgrawopreg1  30643  frgrawopreg2  30644  bj-disjdif  32446