Theorem difeq2 2154

Description: Equality theorem for class difference.

Assertion

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

Proof of Theorem difeq2

Step	Hyp	Ref	Expression
1		eleq2 1535	. . . . 5 |- (A = B -> (x e. A <-> x e. B))
2	1	negbid 611	. . . 4 |- (A = B -> (-. x e. A <-> -. x e. B))
3	2	anbi2d 616	. . 3 |- (A = B -> ((x e. C /\ -. x e. A) <-> (x e. C /\ -. x e. B)))
4	3	abbidv 1577	. 2 |- (A = B -> {x | (x e. C /\ -. x e. A)} = {x | (x e. C /\ -. x e. B)})
5		df-dif 2049	. 2 |- (C \ A) = {x | (x e. C /\ -. x e. A)}
6		df-dif 2049	. 2 |- (C \ B) = {x | (x e. C /\ -. x e. B)}
7	4, 5, 6	3eqtr4g 1531	1 |- (A = B -> (C \ A) = (C \ B))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   = wceq 956   e. wcel 958  {cab 1463   \ cdif 2044

This theorem is referenced by:  difeq2i 2156  difeq2d 2159  oev 4153  sbthlem2 4448  sbth 4457  phplem4 4511  unfilem3 4550  numthlem 4783  numth 4784  fctopOLD 7650  cctop 7652  iscld 7669  islp2 7747  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem4 10591  rcfpfillem4OLD 10592  rcfpfillem5 10593  rcfpfillem5OLD 10594  rcfpfillem6 10595  rcfpfillem6OLD 10596

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-dif 2049

Copyright terms: Public domain