Theorem difeq1 3615

Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
difeq1	|- ( A = B -> ( A \ C ) = ( B \ C ) )

Proof of Theorem difeq1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabeq 3107	. 2 |- ( A = B -> { x e. A | -. x e. C } = { x e. B | -. x e. C } )
2		dfdif2 3485	. 2 |- ( A \ C ) = { x e. A | -. x e. C }
3		dfdif2 3485	. 2 |- ( B \ C ) = { x e. B | -. x e. C }
4	1, 2, 3	3eqtr4g 2533	1 |- ( A = B -> ( A \ C ) = ( B \ C ) )

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-nfc 2617  df-rab 2823  df-dif 3479

This theorem is referenced by:  difeq12  3617  difeq1i  3618  difeq1d  3621  uneqdifeq  3915  hartogslem1  7966  kmlem9  8537  kmlem11  8539  kmlem12  8540  isfin1a  8671  fin1a2lem13  8791  incexclem  13610  ismri  14885  f1otrspeq  16275  pmtrval  16279  pmtrfrn  16286  symgsssg  16295  symgfisg  16296  symggen  16298  psgnunilem1  16321  psgnunilem5  16322  psgneldm  16331  ablfac1eulem  16922  islbs  17517  lbsextlem1  17599  lbsextlem2  17600  lbsextlem3  17601  lbsextlem4  17602  zrhcofipsgn  18412  submafval  18864  m1detdiag  18882  lpval  19422  bwthOLD  19693  2ndcdisj  19739  isufil  20155  ptcmplem2  20304  mblsplit  21694  voliunlem3  21713  ig1pval  22324  nb3graprlem2  24144  iscusgra  24148  isuvtx  24180  isfrgra  24682  1vwmgra  24695  3vfriswmgra  24697  difeq  27106  sigaval  27766  issiga  27767  issgon  27779  probun  28014  ballotlemgval  28118  cvmscbv  28359  cvmsi  28366  cvmsval  28367  symdifeq1  29063  sdrgacs  30771  compne  30943  ldepsnlinc  32199