Theorem nelun

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

	Ref	Expression
Assertion	nelun	⊢ ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( ¬ 𝑋 ∈ 𝐴 ↔ ( ¬ 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( 𝑋 ∈ 𝐴 ↔ 𝑋 ∈ ( 𝐵 ∪ 𝐶 ) ) )
2		elun	⊢ ( 𝑋 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶 ) )
3	1 2	bitrdi	⊢ ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( 𝑋 ∈ 𝐴 ↔ ( 𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶 ) ) )
4	3	notbid	⊢ ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( ¬ 𝑋 ∈ 𝐴 ↔ ¬ ( 𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶 ) ) )
5		ioran	⊢ ( ¬ ( 𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶 ) ↔ ( ¬ 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝐶 ) )
6	4 5	bitrdi	⊢ ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( ¬ 𝑋 ∈ 𝐴 ↔ ( ¬ 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝐶 ) ) )