Theorem bj-inxpALT

Description: Alternate proof of inxp not depending on df-rel . The main proof inxp is shorter because it benefits from the efficient machinery developed for relations: one shows that a class is a relation using theorems like relxp , relinxp , relin1 , relres , and then uses the generic properties of relations, in particular ordered-pair extensionality eqrelriiv . This illustrates the fact that the definitions of Cartesian product df-xp , restriction df-res , and relation df-rel are closely intertwined. Note however that one could use a variant of eqrelriiv not using the Rel predicate, as in bj-ssrel . (Contributed by BJ, 24-Oct-2026) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( z = <. x , y >. -> ( z e. ( ( A X. B ) i^i ( C X. D ) ) <-> <. x , y >. e. ( ( A X. B ) i^i ( C X. D ) ) ) )
2		elin	|- ( <. x , y >. e. ( ( A X. B ) i^i ( C X. D ) ) <-> ( <. x , y >. e. ( A X. B ) /\ <. x , y >. e. ( C X. D ) ) )
3	1 2	bitrdi	|- ( z = <. x , y >. -> ( z e. ( ( A X. B ) i^i ( C X. D ) ) <-> ( <. x , y >. e. ( A X. B ) /\ <. x , y >. e. ( C X. D ) ) ) )
4		an4	|- ( ( ( x e. A /\ x e. C ) /\ ( y e. B /\ y e. D ) ) <-> ( ( x e. A /\ y e. B ) /\ ( x e. C /\ y e. D ) ) )
5		elin	|- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
6		elin	|- ( y e. ( B i^i D ) <-> ( y e. B /\ y e. D ) )
7	5 6	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 ) ) )
8		opelxp	|- ( <. x , y >. e. ( A X. B ) <-> ( x e. A /\ y e. B ) )
9		opelxp	|- ( <. x , y >. e. ( C X. D ) <-> ( x e. C /\ y e. D ) )
10	8 9	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 ) ) )
11	4 7 10	3bitr4ri	|- ( ( <. x , y >. e. ( A X. B ) /\ <. x , y >. e. ( C X. D ) ) <-> ( x e. ( A i^i C ) /\ y e. ( B i^i D ) ) )
12	3 11	bitrdi	|- ( z = <. x , y >. -> ( z e. ( ( A X. B ) i^i ( C X. D ) ) <-> ( x e. ( A i^i C ) /\ y e. ( B i^i D ) ) ) )
13	12	copsex2gb	|- ( E. x E. y ( z = <. x , y >. /\ ( x e. ( A i^i C ) /\ y e. ( B i^i D ) ) ) <-> ( z e. ( _V X. _V ) /\ z e. ( ( A X. B ) i^i ( C X. D ) ) ) )
14		elxp	|- ( z e. ( ( A i^i C ) X. ( B i^i D ) ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. ( A i^i C ) /\ y e. ( B i^i D ) ) ) )
15		xpss	|- ( A X. B ) C_ ( _V X. _V )
16		elinel1	|- ( z e. ( ( A X. B ) i^i ( C X. D ) ) -> z e. ( A X. B ) )
17	15 16	sselid	|- ( z e. ( ( A X. B ) i^i ( C X. D ) ) -> z e. ( _V X. _V ) )
18	17	pm4.71ri	|- ( z e. ( ( A X. B ) i^i ( C X. D ) ) <-> ( z e. ( _V X. _V ) /\ z e. ( ( A X. B ) i^i ( C X. D ) ) ) )
19	13 14 18	3bitr4ri	|- ( z e. ( ( A X. B ) i^i ( C X. D ) ) <-> z e. ( ( A i^i C ) X. ( B i^i D ) ) )
20	19	eqriv	|- ( ( A X. B ) i^i ( C X. D ) ) = ( ( A i^i C ) X. ( B i^i D ) )