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 bitrid 
 |-  ( A e. V -> ( A `' _E B <-> B e. A ) )