Metamath Proof Explorer


Theorem eccnvep

Description: The converse epsilon coset of a set is the set. (Contributed by Peter Mazsa, 27-Jan-2019)

Ref Expression
Assertion eccnvep A V A E -1 = A

Proof

Step Hyp Ref Expression
1 eleccnvep A V x A E -1 x A
2 1 eqrdv A V A E -1 = A