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 ) )