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

Metamath Proof Explorer

Theorem idinxpss

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

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

Proof

Step	Hyp	Ref	Expression
1		inxpss	$⊢ I \cap (A \times B) \subseteq R \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 \leftrightarrow \forall x \in A \forall y \in B (x = y \to x R y)$