Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
General Set Theory
Unordered pairs
inpr0
Next ⟩
neldifpr1
Metamath Proof Explorer
Ascii
Unicode
Theorem
inpr0
Description:
Rewrite an empty intersection with a pair.
(Contributed by
Thierry Arnoux
, 20-Nov-2023)
Ref
Expression
Assertion
inpr0
⊢
A
∩
B
C
=
∅
↔
¬
B
∈
A
∧
¬
C
∈
A
Proof
Step
Hyp
Ref
Expression
1
r19.26
⊢
∀
x
∈
A
x
≠
B
∧
x
≠
C
↔
∀
x
∈
A
x
≠
B
∧
∀
x
∈
A
x
≠
C
2
nelpr
⊢
x
∈
V
→
¬
x
∈
B
C
↔
x
≠
B
∧
x
≠
C
3
2
elv
⊢
¬
x
∈
B
C
↔
x
≠
B
∧
x
≠
C
4
3
imbi2i
⊢
x
∈
A
→
¬
x
∈
B
C
↔
x
∈
A
→
x
≠
B
∧
x
≠
C
5
4
albii
⊢
∀
x
x
∈
A
→
¬
x
∈
B
C
↔
∀
x
x
∈
A
→
x
≠
B
∧
x
≠
C
6
disj1
⊢
A
∩
B
C
=
∅
↔
∀
x
x
∈
A
→
¬
x
∈
B
C
7
df-ral
⊢
∀
x
∈
A
x
≠
B
∧
x
≠
C
↔
∀
x
x
∈
A
→
x
≠
B
∧
x
≠
C
8
5
6
7
3bitr4i
⊢
A
∩
B
C
=
∅
↔
∀
x
∈
A
x
≠
B
∧
x
≠
C
9
nelb
⊢
¬
B
∈
A
↔
∀
x
∈
A
x
≠
B
10
nelb
⊢
¬
C
∈
A
↔
∀
x
∈
A
x
≠
C
11
9
10
anbi12i
⊢
¬
B
∈
A
∧
¬
C
∈
A
↔
∀
x
∈
A
x
≠
B
∧
∀
x
∈
A
x
≠
C
12
1
8
11
3bitr4i
⊢
A
∩
B
C
=
∅
↔
¬
B
∈
A
∧
¬
C
∈
A