Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Miscellanea
inn0
Next ⟩
elintd
Metamath Proof Explorer
Ascii
Unicode
Theorem
inn0
Description:
A nonempty intersection.
(Contributed by
Glauco Siliprandi
, 24-Dec-2020)
Ref
Expression
Assertion
inn0
⊢
A
∩
B
≠
∅
↔
∃
x
∈
A
x
∈
B
Proof
Step
Hyp
Ref
Expression
1
nfcv
⊢
Ⅎ
_
x
A
2
nfcv
⊢
Ⅎ
_
x
B
3
1
2
inn0f
⊢
A
∩
B
≠
∅
↔
∃
x
∈
A
x
∈
B