Theorem brcosscnvcoss

Description: For sets, the A and B cosets by R binary relation and the B and A cosets by R binary relation are the same. (Contributed by Peter Mazsa, 27-Dec-2018)

	Ref	Expression
Assertion	brcosscnvcoss	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ 𝐵 ≀ 𝑅 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		exancom	⊢ ( ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑅 𝐴 ) )
2	1	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑅 𝐴 ) ) )
3		brcoss	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ) )
4		brcoss	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐵 ≀ 𝑅 𝐴 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑅 𝐴 ) ) )
5	4	ancoms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ≀ 𝑅 𝐴 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑅 𝐴 ) ) )
6	2 3 5	3bitr4d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ 𝐵 ≀ 𝑅 𝐴 ) )