ecres2

Description: The restricted coset of B when B is an element of the restriction. (Contributed by Peter Mazsa, 16-Oct-2018)

		Ref	Expression
	Assertion	ecres2	$⊢ B \in A \to [B] ({R ↾}_{A}) = [B] R$

Step	Hyp	Ref	Expression
1		elecres	$⊢ y \in V \to (y \in [B] ({R ↾}_{A}) \leftrightarrow (B \in A \land B R y))$
2	1	elv	$⊢ y \in [B] ({R ↾}_{A}) \leftrightarrow (B \in A \land B R y)$
3	2	baib	$⊢ B \in A \to (y \in [B] ({R ↾}_{A}) \leftrightarrow B R y)$
4	3	eqabdv	$⊢ B \in A \to [B] ({R ↾}_{A}) = \{y \| B R y\}$
5		dfec2	$⊢ B \in A \to [B] R = \{y \| B R y\}$
6	4 5	eqtr4d	$⊢ B \in A \to [B] ({R ↾}_{A}) = [B] R$

Metamath Proof Explorer