Metamath Proof Explorer


Theorem inn0

Description: A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Assertion inn0 ( ( 𝐴𝐵 ) ≠ ∅ ↔ ∃ 𝑥𝐴 𝑥𝐵 )

Proof

Step Hyp Ref Expression
1 nfcv 𝑥 𝐴
2 nfcv 𝑥 𝐵
3 1 2 inn0f ( ( 𝐴𝐵 ) ≠ ∅ ↔ ∃ 𝑥𝐴 𝑥𝐵 )