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 ( 𝐵𝐴 → [ 𝐵 ] ( E ↾ 𝐴 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 ecres2 ( 𝐵𝐴 → [ 𝐵 ] ( E ↾ 𝐴 ) = [ 𝐵 ] E )
2 eccnvep ( 𝐵𝐴 → [ 𝐵 ] E = 𝐵 )
3 1 2 eqtrd ( 𝐵𝐴 → [ 𝐵 ] ( E ↾ 𝐴 ) = 𝐵 )