inxpss

Description: Two ways to say that an intersection with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019)

		Ref	Expression
	Assertion	inxpss	$⊢ R \cap (A \times B) \subseteq S \leftrightarrow \forall x \in A \forall y \in B (x R y \to x S y)$

Step	Hyp	Ref	Expression
1		brinxp2	$⊢ x (R \cap (A \times B)) y \leftrightarrow ((x \in A \land y \in B) \land x R y)$
2	1	imbi1i	$⊢ (x (R \cap (A \times B)) y \to x S y) \leftrightarrow (((x \in A \land y \in B) \land x R y) \to x S y)$
3		impexp	$⊢ (((x \in A \land y \in B) \land x R y) \to x S y) \leftrightarrow ((x \in A \land y \in B) \to (x R y \to x S y))$
4	2 3	bitri	$⊢ (x (R \cap (A \times B)) y \to x S y) \leftrightarrow ((x \in A \land y \in B) \to (x R y \to x S y))$
5	4	2albii	$⊢ \forall x \forall y (x (R \cap (A \times B)) y \to x S y) \leftrightarrow \forall x \forall y ((x \in A \land y \in B) \to (x R y \to x S y))$
6		relinxp	$⊢ Rel (R \cap (A \times B))$
7		ssrel3	$⊢ Rel (R \cap (A \times B)) \to (R \cap (A \times B) \subseteq S \leftrightarrow \forall x \forall y (x (R \cap (A \times B)) y \to x S y))$
8	6 7	ax-mp	$⊢ R \cap (A \times B) \subseteq S \leftrightarrow \forall x \forall y (x (R \cap (A \times B)) y \to x S y)$
9		r2al	$⊢ \forall x \in A \forall y \in B (x R y \to x S y) \leftrightarrow \forall x \forall y ((x \in A \land y \in B) \to (x R y \to x S y))$
10	5 8 9	3bitr4i	$⊢ R \cap (A \times B) \subseteq S \leftrightarrow \forall x \in A \forall y \in B (x R y \to x S y)$

Metamath Proof Explorer