Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Miscellanea
ndisj2
Next ⟩
zenom
Metamath Proof Explorer
Ascii
Unicode
Theorem
ndisj2
Description:
A non-disjointness condition.
(Contributed by
Glauco Siliprandi
, 17-Aug-2020)
Ref
Expression
Hypothesis
ndisj2.1
⊢
x
=
y
→
B
=
C
Assertion
ndisj2
⊢
¬
Disj
x
∈
A
B
↔
∃
x
∈
A
∃
y
∈
A
x
≠
y
∧
B
∩
C
≠
∅
Proof
Step
Hyp
Ref
Expression
1
ndisj2.1
⊢
x
=
y
→
B
=
C
2
1
disjor
⊢
Disj
x
∈
A
B
↔
∀
x
∈
A
∀
y
∈
A
x
=
y
∨
B
∩
C
=
∅
3
2
notbii
⊢
¬
Disj
x
∈
A
B
↔
¬
∀
x
∈
A
∀
y
∈
A
x
=
y
∨
B
∩
C
=
∅
4
rexnal
⊢
∃
x
∈
A
¬
∀
y
∈
A
x
=
y
∨
B
∩
C
=
∅
↔
¬
∀
x
∈
A
∀
y
∈
A
x
=
y
∨
B
∩
C
=
∅
5
rexnal
⊢
∃
y
∈
A
¬
x
=
y
∨
B
∩
C
=
∅
↔
¬
∀
y
∈
A
x
=
y
∨
B
∩
C
=
∅
6
ioran
⊢
¬
x
=
y
∨
B
∩
C
=
∅
↔
¬
x
=
y
∧
¬
B
∩
C
=
∅
7
df-ne
⊢
x
≠
y
↔
¬
x
=
y
8
df-ne
⊢
B
∩
C
≠
∅
↔
¬
B
∩
C
=
∅
9
7
8
anbi12i
⊢
x
≠
y
∧
B
∩
C
≠
∅
↔
¬
x
=
y
∧
¬
B
∩
C
=
∅
10
6
9
bitr4i
⊢
¬
x
=
y
∨
B
∩
C
=
∅
↔
x
≠
y
∧
B
∩
C
≠
∅
11
10
rexbii
⊢
∃
y
∈
A
¬
x
=
y
∨
B
∩
C
=
∅
↔
∃
y
∈
A
x
≠
y
∧
B
∩
C
≠
∅
12
5
11
bitr3i
⊢
¬
∀
y
∈
A
x
=
y
∨
B
∩
C
=
∅
↔
∃
y
∈
A
x
≠
y
∧
B
∩
C
≠
∅
13
12
rexbii
⊢
∃
x
∈
A
¬
∀
y
∈
A
x
=
y
∨
B
∩
C
=
∅
↔
∃
x
∈
A
∃
y
∈
A
x
≠
y
∧
B
∩
C
≠
∅
14
3
4
13
3bitr2i
⊢
¬
Disj
x
∈
A
B
↔
∃
x
∈
A
∃
y
∈
A
x
≠
y
∧
B
∩
C
≠
∅