Theorem inxp

Description: Intersection of two Cartesian products. Exercise 9 of TakeutiZaring p. 25. (Contributed by NM, 3-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-10 , ax-12 . (Revised by SN, 5-May-2025)

	Ref	Expression
Assertion	inxp	|- ( ( A X. B ) i^i ( C X. D ) ) = ( ( A i^i C ) X. ( B i^i D ) )

Proof

Step	Hyp	Ref	Expression
1		relinxp	|- Rel ( ( A X. B ) i^i ( C X. D ) )
2		relxp	|- Rel ( ( A i^i C ) X. ( B i^i D ) )
3		an4	|- ( ( ( x e. A /\ y e. B ) /\ ( x e. C /\ y e. D ) ) <-> ( ( x e. A /\ x e. C ) /\ ( y e. B /\ y e. D ) ) )
4		opelxp	|- ( <. x , y >. e. ( A X. B ) <-> ( x e. A /\ y e. B ) )
5		opelxp	|- ( <. x , y >. e. ( C X. D ) <-> ( x e. C /\ y e. D ) )
6	4 5	anbi12i	|- ( ( <. x , y >. e. ( A X. B ) /\ <. x , y >. e. ( C X. D ) ) <-> ( ( x e. A /\ y e. B ) /\ ( x e. C /\ y e. D ) ) )
7		elin	|- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
8		elin	|- ( y e. ( B i^i D ) <-> ( y e. B /\ y e. D ) )
9	7 8	anbi12i	|- ( ( x e. ( A i^i C ) /\ y e. ( B i^i D ) ) <-> ( ( x e. A /\ x e. C ) /\ ( y e. B /\ y e. D ) ) )
10	3 6 9	3bitr4i	|- ( ( <. x , y >. e. ( A X. B ) /\ <. x , y >. e. ( C X. D ) ) <-> ( x e. ( A i^i C ) /\ y e. ( B i^i D ) ) )
11		elin	|- ( <. x , y >. e. ( ( A X. B ) i^i ( C X. D ) ) <-> ( <. x , y >. e. ( A X. B ) /\ <. x , y >. e. ( C X. D ) ) )
12		opelxp	|- ( <. x , y >. e. ( ( A i^i C ) X. ( B i^i D ) ) <-> ( x e. ( A i^i C ) /\ y e. ( B i^i D ) ) )
13	10 11 12	3bitr4i	|- ( <. x , y >. e. ( ( A X. B ) i^i ( C X. D ) ) <-> <. x , y >. e. ( ( A i^i C ) X. ( B i^i D ) ) )
14	1 2 13	eqrelriiv	|- ( ( A X. B ) i^i ( C X. D ) ) = ( ( A i^i C ) X. ( B i^i D ) )