Metamath Proof Explorer


Theorem releleccnv

Description: Elementhood in a converse R -coset when R is a relation. (Contributed by Peter Mazsa, 9-Dec-2018)

Ref Expression
Assertion releleccnv ( Rel 𝑅 → ( 𝐴 ∈ [ 𝐵 ] 𝑅𝐴 𝑅 𝐵 ) )

Proof

Step Hyp Ref Expression
1 relcnv Rel 𝑅
2 relelec ( Rel 𝑅 → ( 𝐴 ∈ [ 𝐵 ] 𝑅𝐵 𝑅 𝐴 ) )
3 1 2 ax-mp ( 𝐴 ∈ [ 𝐵 ] 𝑅𝐵 𝑅 𝐴 )
4 relbrcnvg ( Rel 𝑅 → ( 𝐵 𝑅 𝐴𝐴 𝑅 𝐵 ) )
5 3 4 syl5bb ( Rel 𝑅 → ( 𝐴 ∈ [ 𝐵 ] 𝑅𝐴 𝑅 𝐵 ) )