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

Metamath Proof Explorer

Theorem releccnveq

Description: Equality of converse R -coset and converse S -coset when R and S are relations. (Contributed by Peter Mazsa, 27-Jul-2019)

Ref Expression
Assertion releccnveq ⊢ Rel ⁡ R ∧ Rel ⁡ S → A R -1 = B S -1 ↔ ∀ x x R A ↔ x S B

Proof

Step Hyp Ref Expression
1 dfcleq ⊢ A R -1 = B S -1 ↔ ∀ x x ∈ A R -1 ↔ x ∈ B S -1
2 releleccnv ⊢ Rel ⁡ R → x ∈ A R -1 ↔ x R A
3 releleccnv ⊢ Rel ⁡ S → x ∈ B S -1 ↔ x S B
4 2 3 bi2bian9 ⊢ Rel ⁡ R ∧ Rel ⁡ S → x ∈ A R -1 ↔ x ∈ B S -1 ↔ x R A ↔ x S B
5 4 albidv ⊢ Rel ⁡ R ∧ Rel ⁡ S → ∀ x x ∈ A R -1 ↔ x ∈ B S -1 ↔ ∀ x x R A ↔ x S B
6 1 5 bitrid ⊢ Rel ⁡ R ∧ Rel ⁡ S → A R -1 = B S -1 ↔ ∀ x x R A ↔ x S B