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

Metamath Proof Explorer

Theorem brcoss3

Description: Alternate form of the A and B are cosets by R binary relation. (Contributed by Peter Mazsa, 26-Mar-2019)

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

Proof

Step Hyp Ref Expression
1 brcnvg 
 |-  ( ( A e. V /\ u e. _V ) -> ( A `' R u <-> u R A ) )
2 1 elvd 
 |-  ( A e. V -> ( A `' R u <-> u R A ) )
3 brcnvg 
 |-  ( ( B e. W /\ u e. _V ) -> ( B `' R u <-> u R B ) )
4 3 elvd 
 |-  ( B e. W -> ( B `' R u <-> u R B ) )
5 2 4 bi2anan9 
 |-  ( ( A e. V /\ B e. W ) -> ( ( A `' R u /\ B `' R u ) <-> ( u R A /\ u R B ) ) )
6 5 exbidv 
 |-  ( ( A e. V /\ B e. W ) -> ( E. u ( A `' R u /\ B `' R u ) <-> E. u ( u R A /\ u R B ) ) )
7 ecinn0 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] `' R i^i [ B ] `' R ) =/= (/) <-> E. u ( A `' R u /\ B `' R u ) ) )
8 brcoss 
 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ R B <-> E. u ( u R A /\ u R B ) ) )
9 6 7 8 3bitr4rd 
 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ R B <-> ( [ A ] `' R i^i [ B ] `' R ) =/= (/) ) )