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	⊢ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) = ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) ) )
2		elin	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ) )
3	1 2	bitrdi	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ) ) )
4		an4	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
5		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) )
6		elin	⊢ ( 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) )
7	5 6	anbi12i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
8		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
9		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) )
10	8 9	anbi12i	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
11	4 7 10	3bitr4ri	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 × 𝐷 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) )
12	3 11	bitrdi	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) ) )
13	12	copsex2gb	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) ) ↔ ( 𝑧 ∈ ( V × V ) ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) ) )
14		elxp	⊢ ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐷 ) ) ) )
15		xpss	⊢ ( 𝐴 × 𝐵 ) ⊆ ( V × V )
16		elinel1	⊢ ( 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) → 𝑧 ∈ ( 𝐴 × 𝐵 ) )
17	15 16	sselid	⊢ ( 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) → 𝑧 ∈ ( V × V ) )
18	17	pm4.71ri	⊢ ( 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) ↔ ( 𝑧 ∈ ( V × V ) ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) ) )
19	13 14 18	3bitr4ri	⊢ ( 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) ↔ 𝑧 ∈ ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) ) )
20	19	eqriv	⊢ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) = ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) )