This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

		Ref	Expression
	Assertion	dmxp	$⊢ B \neq \emptyset \to dom (A \times B) = A$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2	1	eldm	$⊢ x \in dom (A \times B) \leftrightarrow \exists y x (A \times B) y$
3		brxp	$⊢ x (A \times B) y \leftrightarrow (x \in A \land y \in B)$
4	3	exbii	$⊢ \exists y x (A \times B) y \leftrightarrow \exists y (x \in A \land y \in B)$
5		19.42v	$⊢ \exists y (x \in A \land y \in B) \leftrightarrow (x \in A \land \exists y y \in B)$
6	2 4 5	3bitri	$⊢ x \in dom (A \times B) \leftrightarrow (x \in A \land \exists y y \in B)$
7		n0	$⊢ B \neq \emptyset \leftrightarrow \exists y y \in B$
8	7	biimpi	$⊢ B \neq \emptyset \to \exists y y \in B$
9	8	biantrud	$⊢ B \neq \emptyset \to (x \in A \leftrightarrow (x \in A \land \exists y y \in B))$
10	6 9	bitr4id	$⊢ B \neq \emptyset \to (x \in dom (A \times B) \leftrightarrow x \in A)$
11	10	eqrdv	$⊢ B \neq \emptyset \to dom (A \times B) = A$