inxp2

Description: Intersection with a Cartesian product. (Contributed by Peter Mazsa, 18-Jul-2019)

		Ref	Expression
	Assertion	inxp2	$⊢ R \cap (A \times B) = \{⟨x, y⟩ \| ((x \in A \land y \in B) \land x R y)\}$

Step	Hyp	Ref	Expression
1		relinxp	$⊢ Rel (R \cap (A \times B))$
2		dfrel4v	$⊢ Rel (R \cap (A \times B)) \leftrightarrow R \cap (A \times B) = \{⟨x, y⟩ \| x (R \cap (A \times B)) y\}$
3	1 2	mpbi	$⊢ R \cap (A \times B) = \{⟨x, y⟩ \| x (R \cap (A \times B)) y\}$
4		brinxp2	$⊢ x (R \cap (A \times B)) y \leftrightarrow ((x \in A \land y \in B) \land x R y)$
5	4	opabbii	$⊢ \{⟨x, y⟩ \| x (R \cap (A \times B)) y\} = \{⟨x, y⟩ \| ((x \in A \land y \in B) \land x R y)\}$
6	3 5	eqtri	$⊢ R \cap (A \times B) = \{⟨x, y⟩ \| ((x \in A \land y \in B) \land x R y)\}$

Metamath Proof Explorer