Theorem difeq2 3465

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 2502	. . . 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 2962	. 2 |- ( A = B -> { x e. C | -. x e. A } = { x e. C | -. x e. B } )
4		dfdif2 3334	. 2 |- ( C \ A ) = { x e. C | -. x e. A }
5		dfdif2 3334	. 2 |- ( C \ B ) = { x e. C | -. x e. B }
6	3, 4, 5	3eqtr4g 2498	1 |- ( A = B -> ( C \ A ) = ( C \ B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1364   e. wcel 1761   {crab 2717   \ cdif 3322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-ral 2718  df-rab 2722  df-dif 3328

This theorem is referenced by:  difeq12  3466  difeq2i  3468  difeq2d  3471  ssdifeq0  3758  sorpsscmpl  6370  2oconcl  6939  oev  6950  sbthlem2  7418  sbth  7427  infdiffi  7859  fin1ai  8458  fin23lem7  8481  fin23lem11  8482  compsscnv  8536  isf34lem1  8537  compss  8541  isf34lem4  8542  fin1a2lem7  8571  pwfseqlem4a  8824  pwfseqlem4  8825  efgmval  16202  efgi  16209  frgpuptinv  16261  gsumcllem  16379  gsumcllemOLD  16380  gsumzaddlem  16401  gsumzaddlemOLD  16403  fctop  18567  cctop  18569  iscld  18590  clsval2  18613  opncldf1  18647  opncldf2  18648  opncldf3  18649  indiscld  18654  mretopd  18655  restcld  18735  lecldbas  18782  pnrmopn  18906  hauscmplem  18968  elpt  19104  elptr  19105  ptbasfi  19113  cfinfil  19425  csdfil  19426  ufilss  19437  filufint  19452  cfinufil  19460  ufinffr  19461  ufilen  19462  prdsxmslem2  20063  lebnumlem1  20492  bcth3  20801  ismbl  20968  disjdifprg  25854  0elsiga  26493  prsiga  26510  sigaclci  26511  difelsiga  26512  ballotlemfval  26802  ballotlemgval  26836  kur14lem1  27024  symdifeq1  27780  frgrawopreg1  30568  frgrawopreg2  30569  bj-disjdif  32176