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

Metamath Proof Explorer

Theorem idinxpssinxp

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

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

Proof

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