Theorem difeq2 2719

Description: Equality theorem for class difference. (The proof was shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

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

Proof of Theorem difeq2

Step	Hyp	Ref	Expression
1		eleq2 1958	. . . 4 |- (A = B -> (x e. A <-> x e. B))
2	1	notbid 673	. . 3 |- (A = B -> (-. x e. A <-> -. x e. B))
3	2	rabbidv 2287	. 2 |- (A = B -> {x e. C | -. x e. A} = {x e. C | -. x e. B})
4		dfdif2 2608	. 2 |- (C \ A) = {x e. C | -. x e. A}
5		dfdif2 2608	. 2 |- (C \ B) = {x e. C | -. x e. B}
6	3, 4, 5	3eqtr4g 1953	1 |- (A = B -> (C \ A) = (C \ B))

Syntax hints:  -. wn 2   -> wi 3   = wceq 1298   e. wcel 1300  {crab 2108   \ cdif 2590

This theorem is referenced by:  difeq12 2721  difeq2i 2723  difeq2d 2726  resdif 4659  oev 5198  sbthlem2 5511  sbth 5520  phplem4 5605  unfilem3 5643  numthlem 5945  numth 5946  fctop 8920  cctop 8922  iscld 8945  islp2 9023  subcld 10254  rcfpfillem3 14930  rcfpfillem4 14931  rcfpfillem5 14932  rcfpfillem6 14933  clindistop 14962  singempcon 14965  opncldf1 15402  opncldf2 15403  opncldf3 15404  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  isufil2 15565  ufilss 15567  ufileulem 15572  ufileu 15573  filufint 15574  ufinffr 15578  ufilen 15579  filcon 15580  fcluscf 15612  flimfnfcls 15615  heiborlem9 15963

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-rab 2112  df-dif 2597

Copyright terms: Public domain