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) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 12-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	eldm	$$⊢x\in \mathrm{dom}\left(A\times B\right)\leftrightarrow \exists yx\left(A\times B\right)y$$
3		brxp	$$⊢x\left(A\times B\right)y\leftrightarrow \left(x\in A\wedge y\in B\right)$$
4	3	exbii	$$⊢\exists yx\left(A\times B\right)y\leftrightarrow \exists y\left(x\in A\wedge y\in B\right)$$
5		19.42v	$$⊢\exists y\left(x\in A\wedge y\in B\right)\leftrightarrow \left(x\in A\wedge \exists yy\in B\right)$$
6	2 4 5	3bitri	$$⊢x\in \mathrm{dom}\left(A\times B\right)\leftrightarrow \left(x\in A\wedge \exists yy\in B\right)$$
7		n0	$$⊢B\ne \varnothing \leftrightarrow \exists yy\in B$$
8	7	biimpi	$$⊢B\ne \varnothing \to \exists yy\in B$$
9	8	biantrud	$$⊢B\ne \varnothing \to \left(x\in A\leftrightarrow \left(x\in A\wedge \exists yy\in B\right)\right)$$
10	6 9	bitr4id	$$⊢B\ne \varnothing \to \left(x\in \mathrm{dom}\left(A\times B\right)\leftrightarrow x\in A\right)$$
11	10	eqrdv	$$⊢B\ne \varnothing \to \mathrm{dom}\left(A\times B\right)=A$$