inxprnres

Description: Restriction of a class as a class of ordered pairs. (Contributed by Peter Mazsa, 2-Jan-2019)

		Ref	Expression
	Assertion	inxprnres	$⊢ R \cap (A \times ran ({R ↾}_{A})) = \{⟨x, y⟩ \| (x \in A \land x R y)\}$

Step	Hyp	Ref	Expression
1		relinxp	$⊢ Rel (R \cap (A \times ran ({R ↾}_{A})))$
2		relopabv	$⊢ Rel \{⟨x, y⟩ \| (x \in A \land x R y)\}$
3		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
4		breq1	$⊢ x = z \to (x R y \leftrightarrow z R y)$
5	3 4	anbi12d	$⊢ x = z \to ((x \in A \land x R y) \leftrightarrow (z \in A \land z R y))$
6		breq2	$⊢ y = w \to (z R y \leftrightarrow z R w)$
7	6	anbi2d	$⊢ y = w \to ((z \in A \land z R y) \leftrightarrow (z \in A \land z R w))$
8	5 7	opelopabg	$⊢ (z \in V \land w \in V) \to (⟨z, w⟩ \in \{⟨x, y⟩ \| (x \in A \land x R y)\} \leftrightarrow (z \in A \land z R w))$
9	8	el2v	$⊢ ⟨z, w⟩ \in \{⟨x, y⟩ \| (x \in A \land x R y)\} \leftrightarrow (z \in A \land z R w)$
10		brinxprnres	$⊢ w \in V \to (z (R \cap (A \times ran ({R ↾}_{A}))) w \leftrightarrow (z \in A \land z R w))$
11	10	elv	$⊢ z (R \cap (A \times ran ({R ↾}_{A}))) w \leftrightarrow (z \in A \land z R w)$
12		df-br	$⊢ z (R \cap (A \times ran ({R ↾}_{A}))) w \leftrightarrow ⟨z, w⟩ \in (R \cap (A \times ran ({R ↾}_{A})))$
13	9 11 12	3bitr2ri	$⊢ ⟨z, w⟩ \in (R \cap (A \times ran ({R ↾}_{A}))) \leftrightarrow ⟨z, w⟩ \in \{⟨x, y⟩ \| (x \in A \land x R y)\}$
14	1 2 13	eqrelriiv	$⊢ R \cap (A \times ran ({R ↾}_{A})) = \{⟨x, y⟩ \| (x \in A \land x R y)\}$

Metamath Proof Explorer