Theorem difeq2 3530

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 2455	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	notbid 292	. . 3 |- ( A = B -> ( -. x e. A <-> -. x e. B ) )
3	2	rabbidv 3026	. 2 |- ( A = B -> { x e. C | -. x e. A } = { x e. C | -. x e. B } )
4		dfdif2 3398	. 2 |- ( C \ A ) = { x e. C | -. x e. A }
5		dfdif2 3398	. 2 |- ( C \ B ) = { x e. C | -. x e. B }
6	3, 4, 5	3eqtr4g 2448	1 |- ( A = B -> ( C \ A ) = ( C \ B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1399   e. wcel 1826   {crab 2736   \ cdif 3386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-ral 2737  df-rab 2741  df-dif 3392

This theorem is referenced by:  difeq12  3531  difeq2i  3533  difeq2d  3536  symdifeq1  3645  ssdifeq0  3826  sorpsscmpl  6490  2oconcl  7071  oev  7082  sbthlem2  7547  sbth  7556  infdiffi  7988  fin1ai  8586  fin23lem7  8609  fin23lem11  8610  compsscnv  8664  isf34lem1  8665  compss  8669  isf34lem4  8670  fin1a2lem7  8699  pwfseqlem4a  8950  pwfseqlem4  8951  efgmval  16847  efgi  16854  frgpuptinv  16906  gsumcllem  17029  gsumcllemOLD  17030  gsumzaddlem  17051  gsumzaddlemOLD  17053  fctop  19590  cctop  19592  iscld  19613  clsval2  19636  opncldf1  19671  opncldf2  19672  opncldf3  19673  indiscld  19678  mretopd  19679  restcld  19759  lecldbas  19806  pnrmopn  19930  hauscmplem  19992  elpt  20158  elptr  20159  ptbasfi  20167  cfinfil  20479  csdfil  20480  ufilss  20491  filufint  20506  cfinufil  20514  ufinffr  20515  ufilen  20516  prdsxmslem2  21117  lebnumlem1  21546  bcth3  21855  ismbl  22022  frgrawopreg1  25171  frgrawopreg2  25172  disjdifprg  27565  0elsiga  28263  prsiga  28280  sigaclci  28281  difelsiga  28282  sigapildsyslem  28306  sigapildsys  28307  elcarsg  28432  ballotlemfval  28611  ballotlemgval  28645  kur14lem1  28839  dvmptfprodlem  31907  bj-disjdif  34859