Metamath Proof Explorer

Theorem ref5

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

		Ref	Expression
	Assertion	ref5	$⊢ I \cap (A \times B) \subseteq R \leftrightarrow \forall x \in (A \cap B) x R x$

Proof

Step	Hyp	Ref	Expression
1		equcom	$⊢ y = x \leftrightarrow x = y$
2	1	imbi1i	$⊢ (y = x \to x R y) \leftrightarrow (x = y \to x R y)$
3	2	ralbii	$⊢ \forall y \in B (y = x \to x R y) \leftrightarrow \forall y \in B (x = y \to x R y)$
4		breq2	$⊢ y = x \to (x R y \leftrightarrow x R x)$
5	4	ceqsralbv	$⊢ \forall y \in B (y = x \to x R y) \leftrightarrow (x \in B \to x R x)$
6	3 5	bitr3i	$⊢ \forall y \in B (x = y \to x R y) \leftrightarrow (x \in B \to x R x)$
7	6	ralbii	$⊢ \forall x \in A \forall y \in B (x = y \to x R y) \leftrightarrow \forall x \in A (x \in B \to x R x)$
8		idinxpss	$⊢ I \cap (A \times B) \subseteq R \leftrightarrow \forall x \in A \forall y \in B (x = y \to x R y)$
9		ralin	$⊢ \forall x \in (A \cap B) x R x \leftrightarrow \forall x \in A (x \in B \to x R x)$
10	7 8 9	3bitr4i	$⊢ I \cap (A \times B) \subseteq R \leftrightarrow \forall x \in (A \cap B) x R x$