eleccossin

Description: Two ways of saying that the coset of A and the coset of C have the common element B . (Contributed by Peter Mazsa, 15-Oct-2021)

		Ref	Expression
	Assertion	eleccossin	$⊢ (B \in V \land C \in W) \to (B \in ([A] ≀ R \cap [C] ≀ R) \leftrightarrow (A ≀ R B \land B ≀ R C))$

Step	Hyp	Ref	Expression
1		elin	$⊢ B \in ([A] ≀ R \cap [C] ≀ R) \leftrightarrow (B \in [A] ≀ R \land B \in [C] ≀ R)$
2		relcoss	$⊢ Rel ≀ R$
3		relelec	$⊢ Rel ≀ R \to (B \in [A] ≀ R \leftrightarrow A ≀ R B)$
4	2 3	ax-mp	$⊢ B \in [A] ≀ R \leftrightarrow A ≀ R B$
5		relelec	$⊢ Rel ≀ R \to (B \in [C] ≀ R \leftrightarrow C ≀ R B)$
6	2 5	ax-mp	$⊢ B \in [C] ≀ R \leftrightarrow C ≀ R B$
7	4 6	anbi12i	$⊢ (B \in [A] ≀ R \land B \in [C] ≀ R) \leftrightarrow (A ≀ R B \land C ≀ R B)$
8	1 7	bitri	$⊢ B \in ([A] ≀ R \cap [C] ≀ R) \leftrightarrow (A ≀ R B \land C ≀ R B)$
9		brcosscnvcoss	$⊢ (B \in V \land C \in W) \to (B ≀ R C \leftrightarrow C ≀ R B)$
10	9	anbi2d	$⊢ (B \in V \land C \in W) \to ((A ≀ R B \land B ≀ R C) \leftrightarrow (A ≀ R B \land C ≀ R B))$
11	8 10	bitr4id	$⊢ (B \in V \land C \in W) \to (B \in ([A] ≀ R \cap [C] ≀ R) \leftrightarrow (A ≀ R B \land B ≀ R C))$

Metamath Proof Explorer