# Metamath Proof Explorer

## 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 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({A}\wr {R}{B}↔{B}\wr {R}{A}\right)$

### Proof

Step Hyp Ref Expression
1 exancom ${⊢}\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}{R}{A}\wedge {u}{R}{B}\right)↔\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}{R}{B}\wedge {u}{R}{A}\right)$
2 1 a1i ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}{R}{A}\wedge {u}{R}{B}\right)↔\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}{R}{B}\wedge {u}{R}{A}\right)\right)$
3 brcoss ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({A}\wr {R}{B}↔\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}{R}{A}\wedge {u}{R}{B}\right)\right)$
4 brcoss ${⊢}\left({B}\in {W}\wedge {A}\in {V}\right)\to \left({B}\wr {R}{A}↔\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}{R}{B}\wedge {u}{R}{A}\right)\right)$
5 4 ancoms ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({B}\wr {R}{A}↔\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}{R}{B}\wedge {u}{R}{A}\right)\right)$
6 2 3 5 3bitr4d ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({A}\wr {R}{B}↔{B}\wr {R}{A}\right)$