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 e. V -> [ A ] `' _E = A )

Proof

Step Hyp Ref Expression
1 eleccnvep 
 |-  ( A e. V -> ( x e. [ A ] `' _E <-> x e. A ) )
2 1 eqrdv 
 |-  ( A e. V -> [ A ] `' _E = A )