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

Metamath Proof Explorer

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