Theorem difeq1 3418

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 2910	. 2 |- ( A = B -> { x e. A | -. x e. C } = { x e. B | -. x e. C } )
2		dfdif2 3289	. 2 |- ( A \ C ) = { x e. A | -. x e. C }
3		dfdif2 3289	. 2 |- ( B \ C ) = { x e. B | -. x e. C }
4	1, 2, 3	3eqtr4g 2461	1 |- ( A = B -> ( A \ C ) = ( B \ C ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1649   e. wcel 1721   {crab 2670   \ cdif 3277

This theorem is referenced by:  difeq12  3420  difeq1i  3421  difeq1d  3424  uneqdifeq  3676  hartogslem1  7467  kmlem9  7994  kmlem11  7996  kmlem12  7997  isfin1a  8128  fin1a2lem13  8248  incexclem  12571  ismri  13811  ablfac1eulem  15585  islbs  16103  lbsextlem1  16185  lbsextlem2  16186  lbsextlem3  16187  lbsextlem4  16188  lpval  17158  2ndcdisj  17472  isufil  17888  ptcmplem2  18037  mblsplit  19381  voliunlem3  19399  ig1pval  20048  nb3graprlem2  21414  iscusgra  21418  isuvtx  21450  difeq  23951  sigaval  24446  issiga  24447  issgon  24459  probun  24630  ballotlemgval  24734  cvmscbv  24898  cvmsi  24905  cvmsval  24906  symdifeq1  25578  f1otrspeq  27258  pmtrval  27262  pmtrfrn  27268  symgsssg  27276  symgfisg  27277  symggen  27279  psgnunilem1  27284  psgnunilem5  27285  psgneldm  27294  sdrgacs  27377  compne  27510  isfrgra  28094  1vwmgra  28107  3vfriswmgra  28109

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-dif 3283