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

Metamath Proof Explorer

Theorem ecinn0

Description: Two ways of saying that the coset of A and the coset of B have some elements in common. (Contributed by Peter Mazsa, 23-Jan-2019)

Ref Expression
Assertion ecinn0 
|- ( ( A e. V /\ B e. W ) -> ( ( [ A ] R i^i [ B ] R ) =/= (/) <-> E. x ( A R x /\ B R x ) ) )

Proof

Step Hyp Ref Expression
1 ecin0 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] R i^i [ B ] R ) = (/) <-> A. x ( A R x -> -. B R x ) ) )
2 1 necon3abid 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] R i^i [ B ] R ) =/= (/) <-> -. A. x ( A R x -> -. B R x ) ) )
3 notnotb 
 |-  ( B R x <-> -. -. B R x )
4 3 anbi2i 
 |-  ( ( A R x /\ B R x ) <-> ( A R x /\ -. -. B R x ) )
5 4 exbii 
 |-  ( E. x ( A R x /\ B R x ) <-> E. x ( A R x /\ -. -. B R x ) )
6 exanali 
 |-  ( E. x ( A R x /\ -. -. B R x ) <-> -. A. x ( A R x -> -. B R x ) )
7 5 6 bitri 
 |-  ( E. x ( A R x /\ B R x ) <-> -. A. x ( A R x -> -. B R x ) )
8 2 7 bitr4di 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] R i^i [ B ] R ) =/= (/) <-> E. x ( A R x /\ B R x ) ) )