Metamath Proof Explorer


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 A B R A = B R

Proof

Step Hyp Ref Expression
1 elecres y V y B R A B A B R y
2 1 elv y B R A B A B R y
3 2 baib B A y B R A B R y
4 3 abbi2dv B A B R A = y | B R y
5 dfec2 B A B R = y | B R y
6 4 5 eqtr4d B A B R A = B R