Set membership equivalence

Stream: new members

[Kamila Szewczyk]

Hi, I have the following assertion: given that a: σ and S: Set σ, and i wish to prove that: a ∈ S ∩ {s | a = s} ↔ a ∈ S. How do i do this?

[Ruben Van de Velde]

Probably start with a lemma that will be called something like docs#Set.mem_inter

[Ruben Van de Velde]

No, I was thinking of docs#Set.mem_inter_iff

[Kamila Szewczyk]

Thanks, exactly what i was looking for!

[Kevin Buzzard]

Does simp close the goal? This looks like something the simplifier could do