Theorem difeq2 3616

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 2540	. . . 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 3105	. 2 |- ( A = B -> { x e. C | -. x e. A } = { x e. C | -. x e. B } )
4		dfdif2 3485	. 2 |- ( C \ A ) = { x e. C | -. x e. A }
5		dfdif2 3485	. 2 |- ( C \ B ) = { x e. C | -. x e. B }
6	3, 4, 5	3eqtr4g 2533	1 |- ( A = B -> ( C \ A ) = ( C \ B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1379   e. wcel 1767   {crab 2818   \ cdif 3473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-rab 2823  df-dif 3479

This theorem is referenced by:  difeq12  3617  difeq2i  3619  difeq2d  3622  ssdifeq0  3909  sorpsscmpl  6575  2oconcl  7153  oev  7164  sbthlem2  7628  sbth  7637  infdiffi  8074  fin1ai  8673  fin23lem7  8696  fin23lem11  8697  compsscnv  8751  isf34lem1  8752  compss  8756  isf34lem4  8757  fin1a2lem7  8786  pwfseqlem4a  9039  pwfseqlem4  9040  efgmval  16536  efgi  16543  frgpuptinv  16595  gsumcllem  16715  gsumcllemOLD  16716  gsumzaddlem  16737  gsumzaddlemOLD  16739  fctop  19299  cctop  19301  iscld  19322  clsval2  19345  opncldf1  19379  opncldf2  19380  opncldf3  19381  indiscld  19386  mretopd  19387  restcld  19467  lecldbas  19514  pnrmopn  19638  hauscmplem  19700  elpt  19836  elptr  19837  ptbasfi  19845  cfinfil  20157  csdfil  20158  ufilss  20169  filufint  20184  cfinufil  20192  ufinffr  20193  ufilen  20194  prdsxmslem2  20795  lebnumlem1  21224  bcth3  21533  ismbl  21700  frgrawopreg1  24755  frgrawopreg2  24756  disjdifprg  27137  0elsiga  27782  prsiga  27799  sigaclci  27800  difelsiga  27801  ballotlemfval  28096  ballotlemgval  28130  kur14lem1  28318  symdifeq1  29075  bj-disjdif  33610