Metamath Proof Explorer


Theorem eccnvepres3

Description: Condition for a restricted converse epsilon coset of a set to be the set itself. (Contributed by Peter Mazsa, 11-May-2021)

Ref Expression
Assertion eccnvepres3 B dom E -1 A B E -1 A = B

Proof

Step Hyp Ref Expression
1 resdmres E -1 dom E -1 A = E -1 A
2 1 eceq2i B E -1 dom E -1 A = B E -1 A
3 eccnvepres2 B dom E -1 A B E -1 dom E -1 A = B
4 2 3 eqtr3id B dom E -1 A B E -1 A = B