Theorem 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 e. A -> [ B ] ( R |` A ) = [ B ] R )

Proof

Step	Hyp	Ref	Expression
1		elecres	|- ( y e. _V -> ( y e. [ B ] ( R |` A ) <-> ( B e. A /\ B R y ) ) )
2	1	elv	|- ( y e. [ B ] ( R |` A ) <-> ( B e. A /\ B R y ) )
3	2	baib	|- ( B e. A -> ( y e. [ B ] ( R |` A ) <-> B R y ) )
4	3	abbi2dv	|- ( B e. A -> [ B ] ( R |` A ) = { y | B R y } )
5		dfec2	|- ( B e. A -> [ B ] R = { y | B R y } )
6	4 5	eqtr4d	|- ( B e. A -> [ B ] ( R |` A ) = [ B ] R )