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 V B A E -1 B A

Proof

Step Hyp Ref Expression
1 relcnv Rel E -1
2 relelec Rel E -1 B A E -1 A E -1 B
3 1 2 ax-mp B A E -1 A E -1 B
4 brcnvep A V A E -1 B B A
5 3 4 syl5bb A V B A E -1 B A