dfres2

Description: Alternate definition of the restriction operation. (Contributed by Mario Carneiro, 5-Nov-2013)

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

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

Metamath Proof Explorer