Metamath Proof Explorer


Theorem 0xp

Description: The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of Monk1 p. 37. (Contributed by NM, 4-Jul-1994)

Ref Expression
Assertion 0xp × A =

Proof

Step Hyp Ref Expression
1 noel ¬ x
2 simprl z = x y x y A x
3 1 2 mto ¬ z = x y x y A
4 3 nex ¬ y z = x y x y A
5 4 nex ¬ x y z = x y x y A
6 elxp z × A x y z = x y x y A
7 5 6 mtbir ¬ z × A
8 7 nel0 × A =