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