Theorem xp11

Description: The Cartesian product of nonempty classes is a one-to-one "function" of its two "arguments". In other words, two Cartesian products, at least one with nonempty factors, are equal if and only if their respective factors are equal. (Contributed by NM, 31-May-2008)

	Ref	Expression
Assertion	xp11	|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( A X. B ) = ( C X. D ) <-> ( A = C /\ B = D ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpnz	|- ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) )
2		anidm	|- ( ( ( A X. B ) =/= (/) /\ ( A X. B ) =/= (/) ) <-> ( A X. B ) =/= (/) )
3		neeq1	|- ( ( A X. B ) = ( C X. D ) -> ( ( A X. B ) =/= (/) <-> ( C X. D ) =/= (/) ) )
4	3	anbi2d	|- ( ( A X. B ) = ( C X. D ) -> ( ( ( A X. B ) =/= (/) /\ ( A X. B ) =/= (/) ) <-> ( ( A X. B ) =/= (/) /\ ( C X. D ) =/= (/) ) ) )
5	2 4	bitr3id	|- ( ( A X. B ) = ( C X. D ) -> ( ( A X. B ) =/= (/) <-> ( ( A X. B ) =/= (/) /\ ( C X. D ) =/= (/) ) ) )
6		eqimss	|- ( ( A X. B ) = ( C X. D ) -> ( A X. B ) C_ ( C X. D ) )
7		ssxpb	|- ( ( A X. B ) =/= (/) -> ( ( A X. B ) C_ ( C X. D ) <-> ( A C_ C /\ B C_ D ) ) )
8	6 7	syl5ibcom	|- ( ( A X. B ) = ( C X. D ) -> ( ( A X. B ) =/= (/) -> ( A C_ C /\ B C_ D ) ) )
9		eqimss2	|- ( ( A X. B ) = ( C X. D ) -> ( C X. D ) C_ ( A X. B ) )
10		ssxpb	|- ( ( C X. D ) =/= (/) -> ( ( C X. D ) C_ ( A X. B ) <-> ( C C_ A /\ D C_ B ) ) )
11	9 10	syl5ibcom	|- ( ( A X. B ) = ( C X. D ) -> ( ( C X. D ) =/= (/) -> ( C C_ A /\ D C_ B ) ) )
12	8 11	anim12d	|- ( ( A X. B ) = ( C X. D ) -> ( ( ( A X. B ) =/= (/) /\ ( C X. D ) =/= (/) ) -> ( ( A C_ C /\ B C_ D ) /\ ( C C_ A /\ D C_ B ) ) ) )
13		an4	|- ( ( ( A C_ C /\ B C_ D ) /\ ( C C_ A /\ D C_ B ) ) <-> ( ( A C_ C /\ C C_ A ) /\ ( B C_ D /\ D C_ B ) ) )
14		eqss	|- ( A = C <-> ( A C_ C /\ C C_ A ) )
15		eqss	|- ( B = D <-> ( B C_ D /\ D C_ B ) )
16	14 15	anbi12i	|- ( ( A = C /\ B = D ) <-> ( ( A C_ C /\ C C_ A ) /\ ( B C_ D /\ D C_ B ) ) )
17	13 16	bitr4i	|- ( ( ( A C_ C /\ B C_ D ) /\ ( C C_ A /\ D C_ B ) ) <-> ( A = C /\ B = D ) )
18	12 17	imbitrdi	|- ( ( A X. B ) = ( C X. D ) -> ( ( ( A X. B ) =/= (/) /\ ( C X. D ) =/= (/) ) -> ( A = C /\ B = D ) ) )
19	5 18	sylbid	|- ( ( A X. B ) = ( C X. D ) -> ( ( A X. B ) =/= (/) -> ( A = C /\ B = D ) ) )
20	19	com12	|- ( ( A X. B ) =/= (/) -> ( ( A X. B ) = ( C X. D ) -> ( A = C /\ B = D ) ) )
21	1 20	sylbi	|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( A X. B ) = ( C X. D ) -> ( A = C /\ B = D ) ) )
22		xpeq12	|- ( ( A = C /\ B = D ) -> ( A X. B ) = ( C X. D ) )
23	21 22	impbid1	|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( A X. B ) = ( C X. D ) <-> ( A = C /\ B = D ) ) )