ecin0

Description: Two ways of saying that the coset of A and the coset of B have no elements in common. (Contributed by Peter Mazsa, 1-Dec-2018)

		Ref	Expression
	Assertion	ecin0	$⊢ (A \in V \land B \in W) \to ([A] R \cap [B] R = \emptyset \leftrightarrow \forall x (A R x \to \neg B R x))$

Step	Hyp	Ref	Expression
1		disj1	$⊢ [A] R \cap [B] R = \emptyset \leftrightarrow \forall x (x \in [A] R \to \neg x \in [B] R)$
2		elecg	$⊢ (x \in V \land A \in V) \to (x \in [A] R \leftrightarrow A R x)$
3	2	el2v1	$⊢ A \in V \to (x \in [A] R \leftrightarrow A R x)$
4	3	adantr	$⊢ (A \in V \land B \in W) \to (x \in [A] R \leftrightarrow A R x)$
5		elecALTV	$⊢ (B \in W \land x \in V) \to (x \in [B] R \leftrightarrow B R x)$
6	5	elvd	$⊢ B \in W \to (x \in [B] R \leftrightarrow B R x)$
7	6	adantl	$⊢ (A \in V \land B \in W) \to (x \in [B] R \leftrightarrow B R x)$
8	7	notbid	$⊢ (A \in V \land B \in W) \to (\neg x \in [B] R \leftrightarrow \neg B R x)$
9	4 8	imbi12d	$⊢ (A \in V \land B \in W) \to ((x \in [A] R \to \neg x \in [B] R) \leftrightarrow (A R x \to \neg B R x))$
10	9	albidv	$⊢ (A \in V \land B \in W) \to (\forall x (x \in [A] R \to \neg x \in [B] R) \leftrightarrow \forall x (A R x \to \neg B R x))$
11	1 10	bitrid	$⊢ (A \in V \land B \in W) \to ([A] R \cap [B] R = \emptyset \leftrightarrow \forall x (A R x \to \neg B R x))$

Metamath Proof Explorer