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 𝑅 ∧ Rel 𝑆 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑆 ↔ ∀ 𝑥 ( 𝑥 𝑅 𝐴𝑥 𝑆 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 dfcleq ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑆 ↔ ∀ 𝑥 ( 𝑥 ∈ [ 𝐴 ] 𝑅𝑥 ∈ [ 𝐵 ] 𝑆 ) )
2 releleccnv ( Rel 𝑅 → ( 𝑥 ∈ [ 𝐴 ] 𝑅𝑥 𝑅 𝐴 ) )
3 releleccnv ( Rel 𝑆 → ( 𝑥 ∈ [ 𝐵 ] 𝑆𝑥 𝑆 𝐵 ) )
4 2 3 bi2bian9 ( ( Rel 𝑅 ∧ Rel 𝑆 ) → ( ( 𝑥 ∈ [ 𝐴 ] 𝑅𝑥 ∈ [ 𝐵 ] 𝑆 ) ↔ ( 𝑥 𝑅 𝐴𝑥 𝑆 𝐵 ) ) )
5 4 albidv ( ( Rel 𝑅 ∧ Rel 𝑆 ) → ( ∀ 𝑥 ( 𝑥 ∈ [ 𝐴 ] 𝑅𝑥 ∈ [ 𝐵 ] 𝑆 ) ↔ ∀ 𝑥 ( 𝑥 𝑅 𝐴𝑥 𝑆 𝐵 ) ) )
6 1 5 syl5bb ( ( Rel 𝑅 ∧ Rel 𝑆 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑆 ↔ ∀ 𝑥 ( 𝑥 𝑅 𝐴𝑥 𝑆 𝐵 ) ) )