seinxp

Description: Intersection of set-like relation with Cartesian product of its field. (Contributed by Mario Carneiro, 22-Jun-2015)

		Ref	Expression
	Assertion	seinxp	$⊢ R Se A \leftrightarrow (R \cap (A \times A)) Se A$

Step	Hyp	Ref	Expression
1		brinxp	$⊢ (y \in A \land x \in A) \to (y R x \leftrightarrow y (R \cap (A \times A)) x)$
2	1	ancoms	$⊢ (x \in A \land y \in A) \to (y R x \leftrightarrow y (R \cap (A \times A)) x)$
3	2	rabbidva	$⊢ x \in A \to \{y \in A \| y R x\} = \{y \in A \| y (R \cap (A \times A)) x\}$
4	3	eleq1d	$⊢ x \in A \to (\{y \in A \| y R x\} \in V \leftrightarrow \{y \in A \| y (R \cap (A \times A)) x\} \in V)$
5	4	ralbiia	$⊢ \forall x \in A \{y \in A \| y R x\} \in V \leftrightarrow \forall x \in A \{y \in A \| y (R \cap (A \times A)) x\} \in V$
6		df-se	$⊢ R Se A \leftrightarrow \forall x \in A \{y \in A \| y R x\} \in V$
7		df-se	$⊢ (R \cap (A \times A)) Se A \leftrightarrow \forall x \in A \{y \in A \| y (R \cap (A \times A)) x\} \in V$
8	5 6 7	3bitr4i	$⊢ R Se A \leftrightarrow (R \cap (A \times A)) Se A$

Metamath Proof Explorer