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=xyxyAx
3 1 2 mto ¬z=xyxyA
4 3 nex ¬yz=xyxyA
5 4 nex ¬xyz=xyxyA
6 elxp z×Axyz=xyxyA
7 5 6 mtbir ¬z×A
8 7 nel0 ×A=