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 elin ⊢ B ∈ A ≀ R ∩ C ≀ R ↔ B ∈ A ≀ R ∧ B ∈ C ≀ R
2 relcoss ⊢ Rel ⁡ ≀ R
3 relelec ⊢ Rel ⁡ ≀ R → B ∈ A ≀ R ↔ A ≀ R B
4 2 3 ax-mp ⊢ B ∈ A ≀ R ↔ A ≀ R B
5 relelec ⊢ Rel ⁡ ≀ R → B ∈ C ≀ R ↔ C ≀ R B
6 2 5 ax-mp ⊢ B ∈ C ≀ R ↔ C ≀ R B
7 4 6 anbi12i ⊢ B ∈ A ≀ R ∧ B ∈ C ≀ R ↔ A ≀ R B ∧ C ≀ R B
8 1 7 bitri ⊢ B ∈ A ≀ R ∩ C ≀ R ↔ A ≀ R B ∧ C ≀ R B
9 brcosscnvcoss ⊢ B ∈ V ∧ C ∈ W → B ≀ R C ↔ C ≀ R B
10 9 anbi2d ⊢ B ∈ V ∧ C ∈ W → A ≀ R B ∧ B ≀ R C ↔ A ≀ R B ∧ C ≀ R B
11 8 10 bitr4id ⊢ B ∈ V ∧ C ∈ W → B ∈ A ≀ R ∩ C ≀ R ↔ A ≀ R B ∧ B ≀ R C