Metamath Proof Explorer

Theorem idinxpssinxp2

Description: Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 4-Mar-2019) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		idinxpresid	$⊢ I \cap (A \times A) = {I ↾}_{A}$
2	1	sseq1i	$⊢ I \cap (A \times A) \subseteq R \cap (A \times A) \leftrightarrow {I ↾}_{A} \subseteq R \cap (A \times A)$
3		idrefALT	$⊢ {I ↾}_{A} \subseteq R \cap (A \times A) \leftrightarrow \forall x \in A x (R \cap (A \times A)) x$
4		brinxp2	$⊢ x (R \cap (A \times A)) x \leftrightarrow ((x \in A \land x \in A) \land x R x)$
5		pm4.24	$⊢ x \in A \leftrightarrow (x \in A \land x \in A)$
6	5	anbi1i	$⊢ (x \in A \land x R x) \leftrightarrow ((x \in A \land x \in A) \land x R x)$
7	4 6	bitr4i	$⊢ x (R \cap (A \times A)) x \leftrightarrow (x \in A \land x R x)$
8	7	ralbii	$⊢ \forall x \in A x (R \cap (A \times A)) x \leftrightarrow \forall x \in A (x \in A \land x R x)$
9	2 3 8	3bitri	$⊢ I \cap (A \times A) \subseteq R \cap (A \times A) \leftrightarrow \forall x \in A (x \in A \land x R x)$
10		ralanid	$⊢ \forall x \in A (x \in A \land x R x) \leftrightarrow \forall x \in A x R x$
11	9 10	bitri	$⊢ I \cap (A \times A) \subseteq R \cap (A \times A) \leftrightarrow \forall x \in A x R x$