Metamath Proof Explorer

Theorem br2coss

Description: Cosets by ,R binary relation. (Contributed by Peter Mazsa, 25-Aug-2019)

Ref Expression
Assertion br2coss 
|- ( ( A e. V /\ B e. W ) -> ( A ,~ ,~ R B <-> ( [ A ] ,~ R i^i [ B ] ,~ R ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 brcoss3 
 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ ,~ R B <-> ( [ A ] `' ,~ R i^i [ B ] `' ,~ R ) =/= (/) ) )
2 cnvcosseq 
 |-  `' ,~ R = ,~ R
3 2 eceq2i 
 |-  [ A ] `' ,~ R = [ A ] ,~ R
4 2 eceq2i 
 |-  [ B ] `' ,~ R = [ B ] ,~ R
5 3 4 ineq12i 
 |-  ( [ A ] `' ,~ R i^i [ B ] `' ,~ R ) = ( [ A ] ,~ R i^i [ B ] ,~ R )
6 5 neeq1i 
 |-  ( ( [ A ] `' ,~ R i^i [ B ] `' ,~ R ) =/= (/) <-> ( [ A ] ,~ R i^i [ B ] ,~ R ) =/= (/) )
7 1 6 bitrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ ,~ R B <-> ( [ A ] ,~ R i^i [ B ] ,~ R ) =/= (/) ) )