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