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

Proof

Step	Hyp	Ref	Expression
1		df-xp	|- ( A X. B ) = { <. y , x >. | ( y e. A /\ x e. B ) }
2	1	dmeqi	|- dom ( A X. B ) = dom { <. y , x >. | ( y e. A /\ x e. B ) }
3		n0	|- ( B =/= (/) <-> E. x x e. B )
4	3	biimpi	|- ( B =/= (/) -> E. x x e. B )
5	4	ralrimivw	|- ( B =/= (/) -> A. y e. A E. x x e. B )
6		dmopab3	|- ( A. y e. A E. x x e. B <-> dom { <. y , x >. | ( y e. A /\ x e. B ) } = A )
7	5 6	sylib	|- ( B =/= (/) -> dom { <. y , x >. | ( y e. A /\ x e. B ) } = A )
8	2 7	syl5eq	|- ( B =/= (/) -> dom ( A X. B ) = A )