Theorem: mem_def (FM2023Exrcise/section05_sets/sheet4.lean)

State before:
X : Type
P : X → Prop
a : X
⊢ a ∈ {x | P x} ↔ P a
Tactic:
rfl
State after:
no goals