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

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' _E
2 relelec 
 |-  ( Rel `' _E -> ( B e. [ A ] `' _E <-> A `' _E B ) )
3 1 2 ax-mp 
 |-  ( B e. [ A ] `' _E <-> A `' _E B )
4 brcnvep 
 |-  ( A e. V -> ( A `' _E B <-> B e. A ) )
5 3 4 syl5bb 
 |-  ( A e. V -> ( B e. [ A ] `' _E <-> B e. A ) )