Theorem difeq2 3520

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 2495	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	notbid 295	. . 3 |- ( A = B -> ( -. x e. A <-> -. x e. B ) )
3	2	rabbidv 3013	. 2 |- ( A = B -> { x e. C | -. x e. A } = { x e. C | -. x e. B } )
4		dfdif2 3388	. 2 |- ( C \ A ) = { x e. C | -. x e. A }
5		dfdif2 3388	. 2 |- ( C \ B ) = { x e. C | -. x e. B }
6	3, 4, 5	3eqtr4g 2487	1 |- ( A = B -> ( C \ A ) = ( C \ B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1437   e. wcel 1872   {crab 2718   \ cdif 3376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-ral 2719  df-rab 2723  df-dif 3382

This theorem is referenced by:  difeq12  3521  difeq2i  3523  difeq2d  3526  symdifeq1  3638  disjdif2  3819  ssdifeq0  3823  sorpsscmpl  6540  2oconcl  7160  oev  7171  sbthlem2  7636  sbth  7645  infdiffi  8115  fin1ai  8674  fin23lem7  8697  fin23lem11  8698  compsscnv  8752  isf34lem1  8753  compss  8757  isf34lem4  8758  fin1a2lem7  8787  pwfseqlem4a  9037  pwfseqlem4  9038  efgmval  17305  efgi  17312  frgpuptinv  17364  gsumcllem  17485  gsumzaddlem  17497  fctop  19961  cctop  19963  iscld  19984  clsval2  20007  opncldf1  20042  opncldf2  20043  opncldf3  20044  indiscld  20049  mretopd  20050  restcld  20130  lecldbas  20177  pnrmopn  20301  hauscmplem  20363  elpt  20529  elptr  20530  cfinfil  20850  csdfil  20851  ufilss  20862  filufint  20877  cfinufil  20885  ufinffr  20886  ufilen  20887  prdsxmslem2  21486  lebnumlem1  21931  lebnumlem1OLD  21934  bcth3  22241  ismbl  22422  ishpg  24743  frgrawopreg1  25720  frgrawopreg2  25721  disjdifprg  28131  0elsiga  28888  prsiga  28905  sigaclci  28906  difelsiga  28907  unelldsys  28932  sigapildsyslem  28935  sigapildsys  28936  ldgenpisyslem1  28937  isros  28942  unelros  28945  difelros  28946  inelsros  28952  diffiunisros  28953  rossros  28954  elcarsg  29089  ballotlemfval  29274  ballotlemgval  29308  ballotlemgvalOLD  29346  kur14lem1  29881  topdifinffinlem  31657  topdifinffin  31658  prsal  38043  saldifcl  38044  caragenel  38167