Metamath Proof Explorer


Theorem eleccnvep

Description: Elementhood in the converse epsilon coset of A is elementhood in A . (Contributed by Peter Mazsa, 27-Jan-2019)

Ref Expression
Assertion eleccnvep ( 𝐴𝑉 → ( 𝐵 ∈ [ 𝐴 ] E ↔ 𝐵𝐴 ) )

Proof

Step Hyp Ref Expression
1 relcnv Rel E
2 relelec ( Rel E → ( 𝐵 ∈ [ 𝐴 ] E ↔ 𝐴 E 𝐵 ) )
3 1 2 ax-mp ( 𝐵 ∈ [ 𝐴 ] E ↔ 𝐴 E 𝐵 )
4 brcnvep ( 𝐴𝑉 → ( 𝐴 E 𝐵𝐵𝐴 ) )
5 3 4 syl5bb ( 𝐴𝑉 → ( 𝐵 ∈ [ 𝐴 ] E ↔ 𝐵𝐴 ) )