Theorem difeq2 3601

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 2516	. . . 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 3087	. 2 |- ( A = B -> { x e. C | -. x e. A } = { x e. C | -. x e. B } )
4		dfdif2 3470	. 2 |- ( C \ A ) = { x e. C | -. x e. A }
5		dfdif2 3470	. 2 |- ( C \ B ) = { x e. C | -. x e. B }
6	3, 4, 5	3eqtr4g 2509	1 |- ( A = B -> ( C \ A ) = ( C \ B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1383   e. wcel 1804   {crab 2797   \ cdif 3458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ral 2798  df-rab 2802  df-dif 3464

This theorem is referenced by:  difeq12  3602  difeq2i  3604  difeq2d  3607  ssdifeq0  3896  sorpsscmpl  6576  2oconcl  7155  oev  7166  sbthlem2  7630  sbth  7639  infdiffi  8077  fin1ai  8676  fin23lem7  8699  fin23lem11  8700  compsscnv  8754  isf34lem1  8755  compss  8759  isf34lem4  8760  fin1a2lem7  8789  pwfseqlem4a  9042  pwfseqlem4  9043  efgmval  16708  efgi  16715  frgpuptinv  16767  gsumcllem  16890  gsumcllemOLD  16891  gsumzaddlem  16912  gsumzaddlemOLD  16914  fctop  19482  cctop  19484  iscld  19505  clsval2  19528  opncldf1  19562  opncldf2  19563  opncldf3  19564  indiscld  19569  mretopd  19570  restcld  19650  lecldbas  19697  pnrmopn  19821  hauscmplem  19883  elpt  20050  elptr  20051  ptbasfi  20059  cfinfil  20371  csdfil  20372  ufilss  20383  filufint  20398  cfinufil  20406  ufinffr  20407  ufilen  20408  prdsxmslem2  21009  lebnumlem1  21438  bcth3  21747  ismbl  21914  frgrawopreg1  25026  frgrawopreg2  25027  disjdifprg  27412  0elsiga  28091  prsiga  28108  sigaclci  28109  difelsiga  28110  ballotlemfval  28405  ballotlemgval  28439  kur14lem1  28627  symdifeq1  29445  bj-disjdif  34259