# 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 ${⊢}\varnothing ×{A}=\varnothing$

### Proof

Step Hyp Ref Expression
1 noel ${⊢}¬{x}\in \varnothing$
2 simprl ${⊢}\left({z}=⟨{x},{y}⟩\wedge \left({x}\in \varnothing \wedge {y}\in {A}\right)\right)\to {x}\in \varnothing$
3 1 2 mto ${⊢}¬\left({z}=⟨{x},{y}⟩\wedge \left({x}\in \varnothing \wedge {y}\in {A}\right)\right)$
4 3 nex ${⊢}¬\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge \left({x}\in \varnothing \wedge {y}\in {A}\right)\right)$
5 4 nex ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge \left({x}\in \varnothing \wedge {y}\in {A}\right)\right)$
6 elxp ${⊢}{z}\in \left(\varnothing ×{A}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge \left({x}\in \varnothing \wedge {y}\in {A}\right)\right)$
7 5 6 mtbir ${⊢}¬{z}\in \left(\varnothing ×{A}\right)$
8 7 nel0 ${⊢}\varnothing ×{A}=\varnothing$