Metamath Proof Explorer


Theorem eccnvepres

Description: Restricted converse epsilon coset of B . (Contributed by Peter Mazsa, 11-Feb-2018) (Revised by Peter Mazsa, 21-Oct-2021)

Ref Expression
Assertion eccnvepres ( 𝐵𝑉 → [ 𝐵 ] ( E ↾ 𝐴 ) = { 𝑥𝐵𝐵𝐴 } )

Proof

Step Hyp Ref Expression
1 brcnvep ( 𝐵𝑉 → ( 𝐵 E 𝑥𝑥𝐵 ) )
2 1 anbi1cd ( 𝐵𝑉 → ( ( 𝐵𝐴𝐵 E 𝑥 ) ↔ ( 𝑥𝐵𝐵𝐴 ) ) )
3 2 abbidv ( 𝐵𝑉 → { 𝑥 ∣ ( 𝐵𝐴𝐵 E 𝑥 ) } = { 𝑥 ∣ ( 𝑥𝐵𝐵𝐴 ) } )
4 ecres [ 𝐵 ] ( E ↾ 𝐴 ) = { 𝑥 ∣ ( 𝐵𝐴𝐵 E 𝑥 ) }
5 df-rab { 𝑥𝐵𝐵𝐴 } = { 𝑥 ∣ ( 𝑥𝐵𝐵𝐴 ) }
6 3 4 5 3eqtr4g ( 𝐵𝑉 → [ 𝐵 ] ( E ↾ 𝐴 ) = { 𝑥𝐵𝐵𝐴 } )