Metamath Proof Explorer

Theorem nelun

Description: Negated membership for a union. (Contributed by Thierry Arnoux, 13-Dec-2023)

Ref Expression
Assertion nelun ⊢ A = B ∪ C → ¬ X ∈ A ↔ ¬ X ∈ B ∧ ¬ X ∈ C

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ A = B ∪ C → X ∈ A ↔ X ∈ B ∪ C
2 elun ⊢ X ∈ B ∪ C ↔ X ∈ B ∨ X ∈ C
3 1 2 bitrdi ⊢ A = B ∪ C → X ∈ A ↔ X ∈ B ∨ X ∈ C
4 3 notbid ⊢ A = B ∪ C → ¬ X ∈ A ↔ ¬ X ∈ B ∨ X ∈ C
5 ioran ⊢ ¬ X ∈ B ∨ X ∈ C ↔ ¬ X ∈ B ∧ ¬ X ∈ C
6 4 5 bitrdi ⊢ A = B ∪ C → ¬ X ∈ A ↔ ¬ X ∈ B ∧ ¬ X ∈ C