Metamath Proof Explorer

Theorem 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 ∈ V ∧ C ∈ W → B ∈ A ≀ R ∩ C ≀ R ↔ A ≀ R B ∧ B ≀ R C

Proof

Step Hyp Ref Expression
1 brcosscnvcoss ⊢ B ∈ V ∧ C ∈ W → B ≀ R C ↔ C ≀ R B
2 1 anbi2d ⊢ B ∈ V ∧ C ∈ W → A ≀ R B ∧ B ≀ R C ↔ A ≀ R B ∧ C ≀ R B
3 elin ⊢ B ∈ A ≀ R ∩ C ≀ R ↔ B ∈ A ≀ R ∧ B ∈ C ≀ R
4 relcoss ⊢ Rel ⁡ ≀ R
5 relelec ⊢ Rel ⁡ ≀ R → B ∈ A ≀ R ↔ A ≀ R B
6 4 5 ax-mp ⊢ B ∈ A ≀ R ↔ A ≀ R B
7 relelec ⊢ Rel ⁡ ≀ R → B ∈ C ≀ R ↔ C ≀ R B
8 4 7 ax-mp ⊢ B ∈ C ≀ R ↔ C ≀ R B
9 6 8 anbi12i ⊢ B ∈ A ≀ R ∧ B ∈ C ≀ R ↔ A ≀ R B ∧ C ≀ R B
10 3 9 bitri ⊢ B ∈ A ≀ R ∩ C ≀ R ↔ A ≀ R B ∧ C ≀ R B
11 2 10 syl6rbbr ⊢ B ∈ V ∧ C ∈ W → B ∈ A ≀ R ∩ C ≀ R ↔ A ≀ R B ∧ B ≀ R C