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 dom A × B = A

Proof

Step Hyp Ref Expression
1 vex x V
2 1 eldm x dom A × B y x A × B y
3 brxp x A × B y x A y B
4 3 exbii y x A × B y y x A y B
5 19.42v y x A y B x A y y B
6 2 4 5 3bitri x dom A × B x A y y B
7 n0 B y y B
8 7 biimpi B y y B
9 8 biantrud B x A x A y y B
10 6 9 bitr4id B x dom A × B x A
11 10 eqrdv B dom A × B = A