Metamath Proof Explorer


Theorem eccnvepres

Description: Restricted converse epsilon coset of B . (Contributed by Peter Mazsa, 11-Feb-2018) (Revised by Peter Mazsa, 21-Oct-2021)

Ref Expression
Assertion eccnvepres B V B E -1 A = x B | B A

Proof

Step Hyp Ref Expression
1 brcnvep B V B E -1 x x B
2 1 anbi1cd B V B A B E -1 x x B B A
3 2 abbidv B V x | B A B E -1 x = x | x B B A
4 ecres B E -1 A = x | B A B E -1 x
5 df-rab x B | B A = x | x B B A
6 3 4 5 3eqtr4g B V B E -1 A = x B | B A