Theorem brcoss

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

	Ref	Expression
Assertion	brcoss	|- ( ( A e. V /\ B e. W ) -> ( A ,~ R B <-> E. u ( u R A /\ u R B ) ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	|- ( x = A -> ( u R x <-> u R A ) )
2		breq2	|- ( y = B -> ( u R y <-> u R B ) )
3	1 2	bi2anan9	|- ( ( x = A /\ y = B ) -> ( ( u R x /\ u R y ) <-> ( u R A /\ u R B ) ) )
4	3	exbidv	|- ( ( x = A /\ y = B ) -> ( E. u ( u R x /\ u R y ) <-> E. u ( u R A /\ u R B ) ) )
5		df-coss	|- ,~ R = { <. x , y >. | E. u ( u R x /\ u R y ) }
6	4 5	brabga	|- ( ( A e. V /\ B e. W ) -> ( A ,~ R B <-> E. u ( u R A /\ u R B ) ) )