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\times B\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		df-xp	$$⊢A\times B=\left\{⟨y,x⟩|\left(y\in A\wedge x\in B\right)\right\}$$
2	1	dmeqi	$$⊢\mathrm{dom}\left(A\times B\right)=\mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge x\in B\right)\right\}$$
3		n0	$$⊢B\ne \varnothing \leftrightarrow \exists xx\in B$$
4	3	biimpi	$$⊢B\ne \varnothing \to \exists xx\in B$$
5	4	ralrimivw	$$⊢B\ne \varnothing \to \forall y\in A\exists xx\in B$$
6		dmopab3	$$⊢\forall y\in A\exists xx\in B\leftrightarrow \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\times B\right)=A$$