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 X. B ) = A )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 eldm 
 |-  ( x e. dom ( A X. B ) <-> E. y x ( A X. B ) y )
3 brxp 
 |-  ( x ( A X. B ) y <-> ( x e. A /\ y e. B ) )
4 3 exbii 
 |-  ( E. y x ( A X. B ) y <-> E. y ( x e. A /\ y e. B ) )
5 19.42v 
 |-  ( E. y ( x e. A /\ y e. B ) <-> ( x e. A /\ E. y y e. B ) )
6 2 4 5 3bitri 
 |-  ( x e. dom ( A X. B ) <-> ( x e. A /\ E. y y e. B ) )
7 n0 
 |-  ( B =/= (/) <-> E. y y e. B )
8 7 biimpi 
 |-  ( B =/= (/) -> E. y y e. B )
9 8 biantrud 
 |-  ( B =/= (/) -> ( x e. A <-> ( x e. A /\ E. y y e. B ) ) )
10 6 9 bitr4id 
 |-  ( B =/= (/) -> ( x e. dom ( A X. B ) <-> x e. A ) )
11 10 eqrdv 
 |-  ( B =/= (/) -> dom ( A X. B ) = A )