Metamath Proof Explorer


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