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 \times B) \cap (C \times D) = (A \cap C) \times (B \cap D)$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ z = ⟨x, y⟩ \to (z \in ((A \times B) \cap (C \times D)) \leftrightarrow ⟨x, y⟩ \in ((A \times B) \cap (C \times D)))$
2		elin	$⊢ ⟨x, y⟩ \in ((A \times B) \cap (C \times D)) \leftrightarrow (⟨x, y⟩ \in (A \times B) \land ⟨x, y⟩ \in (C \times D))$
3	1 2	bitrdi	$⊢ z = ⟨x, y⟩ \to (z \in ((A \times B) \cap (C \times D)) \leftrightarrow (⟨x, y⟩ \in (A \times B) \land ⟨x, y⟩ \in (C \times D)))$
4		an4	$⊢ ((x \in A \land x \in C) \land (y \in B \land y \in D)) \leftrightarrow ((x \in A \land y \in B) \land (x \in C \land y \in D))$
5		elin	$⊢ x \in (A \cap C) \leftrightarrow (x \in A \land x \in C)$
6		elin	$⊢ y \in (B \cap D) \leftrightarrow (y \in B \land y \in D)$
7	5 6	anbi12i	$⊢ (x \in (A \cap C) \land y \in (B \cap D)) \leftrightarrow ((x \in A \land x \in C) \land (y \in B \land y \in D))$
8		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
9		opelxp	$⊢ ⟨x, y⟩ \in (C \times D) \leftrightarrow (x \in C \land y \in D)$
10	8 9	anbi12i	$⊢ (⟨x, y⟩ \in (A \times B) \land ⟨x, y⟩ \in (C \times D)) \leftrightarrow ((x \in A \land y \in B) \land (x \in C \land y \in D))$
11	4 7 10	3bitr4ri	$⊢ (⟨x, y⟩ \in (A \times B) \land ⟨x, y⟩ \in (C \times D)) \leftrightarrow (x \in (A \cap C) \land y \in (B \cap D))$
12	3 11	bitrdi	$⊢ z = ⟨x, y⟩ \to (z \in ((A \times B) \cap (C \times D)) \leftrightarrow (x \in (A \cap C) \land y \in (B \cap D)))$
13	12	copsex2gb	$⊢ \exists x \exists y (z = ⟨x, y⟩ \land (x \in (A \cap C) \land y \in (B \cap D))) \leftrightarrow (z \in (V \times V) \land z \in ((A \times B) \cap (C \times D)))$
14		elxp	$⊢ z \in ((A \cap C) \times (B \cap D)) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in (A \cap C) \land y \in (B \cap D)))$
15		xpss	$⊢ A \times B \subseteq V \times V$
16		elinel1	$⊢ z \in ((A \times B) \cap (C \times D)) \to z \in (A \times B)$
17	15 16	sselid	$⊢ z \in ((A \times B) \cap (C \times D)) \to z \in (V \times V)$
18	17	pm4.71ri	$⊢ z \in ((A \times B) \cap (C \times D)) \leftrightarrow (z \in (V \times V) \land z \in ((A \times B) \cap (C \times D)))$
19	13 14 18	3bitr4ri	$⊢ z \in ((A \times B) \cap (C \times D)) \leftrightarrow z \in ((A \cap C) \times (B \cap D))$
20	19	eqriv	$⊢ (A \times B) \cap (C \times D) = (A \cap C) \times (B \cap D)$

Metamath Proof Explorer

Theorem bj-inxpALT

Proof