Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The empty set
inn0
Next ⟩
difin0ss
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