Theorem brcosscnv

Description: A and B are cosets by converse R : a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019)

	Ref	Expression
Assertion	brcosscnv	|- ( ( A e. V /\ B e. W ) -> ( A ,~ `' R B <-> E. x ( A R x /\ B R x ) ) )

Proof

Step	Hyp	Ref	Expression
1		brcoss	|- ( ( A e. V /\ B e. W ) -> ( A ,~ `' R B <-> E. x ( x `' R A /\ x `' R B ) ) )
2		brcnvg	|- ( ( x e. _V /\ A e. V ) -> ( x `' R A <-> A R x ) )
3	2	el2v1	|- ( A e. V -> ( x `' R A <-> A R x ) )
4		brcnvg	|- ( ( x e. _V /\ B e. W ) -> ( x `' R B <-> B R x ) )
5	4	el2v1	|- ( B e. W -> ( x `' R B <-> B R x ) )
6	3 5	bi2anan9	|- ( ( A e. V /\ B e. W ) -> ( ( x `' R A /\ x `' R B ) <-> ( A R x /\ B R x ) ) )
7	6	exbidv	|- ( ( A e. V /\ B e. W ) -> ( E. x ( x `' R A /\ x `' R B ) <-> E. x ( A R x /\ B R x ) ) )
8	1 7	bitrd	|- ( ( A e. V /\ B e. W ) -> ( A ,~ `' R B <-> E. x ( A R x /\ B R x ) ) )