This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relinxp

Description: Intersection with a Cartesian product is a relation. (Contributed by Peter Mazsa, 4-Mar-2019)

		Ref	Expression
	Assertion	relinxp	$⊢ Rel (R \cap (A \times B))$

Step	Hyp	Ref	Expression
1		relxp	$⊢ Rel (A \times B)$
2		relin2	$⊢ Rel (A \times B) \to Rel (R \cap (A \times B))$
3	1 2	ax-mp	$⊢ Rel (R \cap (A \times B))$