Theorem: Section4sheet4.mem_def (FormalisingMathematics2024/Section04sets/Sheet4.lean)

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