[STATEMENT]
lemma differenceset_translate_eq_left:
  assumes "A \<subseteq> G" and "B \<subseteq> G" and "x \<in> G"
  shows "(differenceset {x} A = differenceset {x} B) \<longleftrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (differenceset {x} A = differenceset {x} B) = (A = B)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
B \<subseteq> G
x \<in> G

goal (1 subgoal):
 1. (differenceset {x} A = differenceset {x} B) = (A = B)
[PROOF STEP]
by (metis differenceset_commute differenceset_translate_eq_right)