# Metamath Proof Explorer

## Theorem dmxp

Description: The domain of a Cartesian product. Part of Theorem 3.13(x) of Monk1 p. 37. (Contributed by NM, 28-Jul-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion dmxp ${⊢}{B}\ne \varnothing \to \mathrm{dom}\left({A}×{B}\right)={A}$

### Proof

Step Hyp Ref Expression
1 df-xp ${⊢}{A}×{B}=\left\{⟨{y},{x}⟩|\left({y}\in {A}\wedge {x}\in {B}\right)\right\}$
2 1 dmeqi ${⊢}\mathrm{dom}\left({A}×{B}\right)=\mathrm{dom}\left\{⟨{y},{x}⟩|\left({y}\in {A}\wedge {x}\in {B}\right)\right\}$
3 n0 ${⊢}{B}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {B}$
4 3 biimpi ${⊢}{B}\ne \varnothing \to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {B}$
5 4 ralrimivw ${⊢}{B}\ne \varnothing \to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {B}$
6 dmopab3 ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {B}↔\mathrm{dom}\left\{⟨{y},{x}⟩|\left({y}\in {A}\wedge {x}\in {B}\right)\right\}={A}$
7 5 6 sylib ${⊢}{B}\ne \varnothing \to \mathrm{dom}\left\{⟨{y},{x}⟩|\left({y}\in {A}\wedge {x}\in {B}\right)\right\}={A}$
8 2 7 syl5eq ${⊢}{B}\ne \varnothing \to \mathrm{dom}\left({A}×{B}\right)={A}$