Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
General Set Theory
Set relations and operations - misc additions
nelun
Next ⟩
snsssng
Metamath Proof Explorer
Ascii
Unicode
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
syl6bb
⊢
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
syl6bb
⊢
A
=
B
∪
C
→
¬
X
∈
A
↔
¬
X
∈
B
∧
¬
X
∈
C