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

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 
|- ( ( A e. V /\ B e. W ) -> ( A ,~ R B <-> B ,~ R A ) )

Proof

Step Hyp Ref Expression
1 exancom 
 |-  ( E. u ( u R A /\ u R B ) <-> E. u ( u R B /\ u R A ) )
2 1 a1i 
 |-  ( ( A e. V /\ B e. W ) -> ( E. u ( u R A /\ u R B ) <-> E. u ( u R B /\ u R A ) ) )
3 brcoss 
 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ R B <-> E. u ( u R A /\ u R B ) ) )
4 brcoss 
 |-  ( ( B e. W /\ A e. V ) -> ( B ,~ R A <-> E. u ( u R B /\ u R A ) ) )
5 4 ancoms 
 |-  ( ( A e. V /\ B e. W ) -> ( B ,~ R A <-> E. u ( u R B /\ u R A ) ) )
6 2 3 5 3bitr4d 
 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ R B <-> B ,~ R A ) )