Metamath Proof Explorer


Theorem brcnvep

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

Ref Expression
Assertion brcnvep
|- ( A e. V -> ( A `' _E B <-> B e. A ) )

Proof

Step Hyp Ref Expression
1 rele
 |-  Rel _E
2 1 relbrcnv
 |-  ( A `' _E B <-> B _E A )
3 epelg
 |-  ( A e. V -> ( B _E A <-> B e. A ) )
4 2 3 syl5bb
 |-  ( A e. V -> ( A `' _E B <-> B e. A ) )