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

Metamath Proof Explorer

Theorem inxpssidinxp

Description: Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 . (Contributed by Peter Mazsa, 4-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		inxpss2	$⊢ R \cap (A \times B) \subseteq I \cap (A \times B) \leftrightarrow \forall x \in A \forall y \in B (x R y \to x I y)$
2		ideqg	$⊢ y \in V \to (x I y \leftrightarrow x = y)$
3	2	elv	$⊢ x I y \leftrightarrow x = y$
4	3	imbi2i	$⊢ (x R y \to x I y) \leftrightarrow (x R y \to x = y)$
5	4	2ralbii	$⊢ \forall x \in A \forall y \in B (x R y \to x I y) \leftrightarrow \forall x \in A \forall y \in B (x R y \to x = y)$
6	1 5	bitri	$⊢ R \cap (A \times B) \subseteq I \cap (A \times B) \leftrightarrow \forall x \in A \forall y \in B (x R y \to x = y)$