Metamath Proof Explorer


Theorem eccnvepres2

Description: The restricted converse epsilon coset of an element of the restriction is the element itself. (Contributed by Peter Mazsa, 16-Jul-2019)

Ref Expression
Assertion eccnvepres2 B A B E -1 A = B

Proof

Step Hyp Ref Expression
1 ecres2 B A B E -1 A = B E -1
2 eccnvep B A B E -1 = B
3 1 2 eqtrd B A B E -1 A = B