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