Theory Collect_Extra

theory Collect_Extra
  imports Main
begin

lemma Collect_if_eq: "{x. if b x then P x else Q x } = {x. b x ∧ P x } ∪ {x. ¬b x ∧ Q x}"
  by auto

lemma Collect_not_mem_conj_eq: "{x. x ∉ X ∧ P x} = {x. P x} - X"
  by auto

end