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 V B W A R B R x A R x B R x

Proof

Step Hyp Ref Expression
1 ecin0 A V B W A R B R = x A R x ¬ B R x
2 1 necon3abid A V B W A R B R ¬ 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 x A R x B R x x A R x ¬ ¬ B R x
6 exanali x A R x ¬ ¬ B R x ¬ x A R x ¬ B R x
7 5 6 bitri x A R x B R x ¬ x A R x ¬ B R x
8 2 7 bitr4di A V B W A R B R x A R x B R x