Theorem difeq1 3546

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1446   e. wcel 1889   {crab 2743   \ cdif 3403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-rab 2748  df-dif 3409

This theorem is referenced by:  difeq12  3548  difeq1i  3549  difeq1d  3552  symdifeq1  3667  uneqdifeq  3858  hartogslem1  8062  kmlem9  8593  kmlem11  8595  kmlem12  8596  isfin1a  8727  fin1a2lem13  8847  incexclem  13906  coprmprod  14690  coprmproddvds  14692  ismri  15549  f1otrspeq  17100  pmtrval  17104  pmtrfrn  17111  symgsssg  17120  symgfisg  17121  symggen  17123  psgnunilem1  17146  psgnunilem5  17147  psgneldm  17156  ablfac1eulem  17717  islbs  18311  lbsextlem1  18393  lbsextlem2  18394  lbsextlem3  18395  lbsextlem4  18396  zrhcofipsgn  19173  submafval  19616  m1detdiag  19634  lpval  20167  2ndcdisj  20483  isufil  20930  ptcmplem2  21080  mblsplit  22498  voliunlem3  22517  ig1pval  23136  ig1pvalOLD  23142  nb3graprlem2  25192  iscusgra  25196  isuvtx  25228  isfrgra  25730  1vwmgra  25743  3vfriswmgra  25745  difeq  28163  sigaval  28944  issiga  28945  issgon  28957  isros  29002  unelros  29005  difelros  29006  inelsros  29012  diffiunisros  29013  rossros  29014  inelcarsg  29155  carsgclctunlem2  29163  probun  29264  ballotlemgval  29368  ballotlemgvalOLD  29406  cvmscbv  29993  cvmsi  30000  cvmsval  30001  poimirlem4  31956  sdrgacs  36079  compne  36804  dvmptfprod  37830  caragensplit  38331  nbgr2vtx1edg  39428  nbuhgr2vtx1edgb  39430  nbgr0vtx  39434  nb3grprlem2  39465  uvtxa01vtx0  39479  cplgr1v  39507  ldepsnlinc  40405