Metamath Proof Explorer


Theorem brcnvep

Description: The converse of the binary epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018)

Ref Expression
Assertion brcnvep ( 𝐴𝑉 → ( 𝐴 E 𝐵𝐵𝐴 ) )

Proof

Step Hyp Ref Expression
1 rele Rel E
2 1 relbrcnv ( 𝐴 E 𝐵𝐵 E 𝐴 )
3 epelg ( 𝐴𝑉 → ( 𝐵 E 𝐴𝐵𝐴 ) )
4 2 3 syl5bb ( 𝐴𝑉 → ( 𝐴 E 𝐵𝐵𝐴 ) )