This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⁡ R → A ∈ B R -1 ↔ A R B

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ⁡ R -1
2 relelec ⊢ Rel ⁡ R -1 → A ∈ B R -1 ↔ B R -1 A
3 1 2 ax-mp ⊢ A ∈ B R -1 ↔ B R -1 A
4 relbrcnvg ⊢ Rel ⁡ R → B R -1 A ↔ A R B
5 3 4 bitrid ⊢ Rel ⁡ R → A ∈ B R -1 ↔ A R B