Metamath Proof Explorer


Theorem 0nelxp

Description: The empty set is not a member of a Cartesian product. (Contributed by NM, 2-May-1996) (Revised by Mario Carneiro, 26-Apr-2015) (Proof shortened by JJ, 13-Aug-2021)

Ref Expression
Assertion 0nelxp ¬ A × B

Proof

Step Hyp Ref Expression
1 vex x V
2 vex y V
3 1 2 opnzi x y
4 3 nesymi ¬ = x y
5 4 intnanr ¬ = x y x A y B
6 5 nex ¬ y = x y x A y B
7 6 nex ¬ x y = x y x A y B
8 elxp A × B x y = x y x A y B
9 7 8 mtbir ¬ A × B