Theorem dmxpOLD

Description: Obsolete version of dmxp as of 19-Dec-2024. (Contributed by NM, 28-Jul-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	dmxpOLD	|- ( 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	eqtrid	|- ( B =/= (/) -> dom ( A X. B ) = A )