Theorem: Section4sheet1.mem_union_iff (FormalisingMathematics2024/Section04sets/Sheet1.lean)

State before:
X : Type
A B C D : Set X
x : X
⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
Tactic:
rfl
State after:
no goals