Metamath Proof Explorer

Theorem br1cossres

Description: B and C are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 30-Dec-2018)

Ref Expression
Assertion br1cossres ⊢ B ∈ V ∧ C ∈ W → B ≀ R ↾ A C ↔ ∃ u ∈ A u R B ∧ u R C

Proof

Step Hyp Ref Expression
1 brcoss ⊢ B ∈ V ∧ C ∈ W → B ≀ R ↾ A C ↔ ∃ u u R ↾ A B ∧ u R ↾ A C
2 exanres ⊢ B ∈ V ∧ C ∈ W → ∃ u u R ↾ A B ∧ u R ↾ A C ↔ ∃ u ∈ A u R B ∧ u R C
3 1 2 bitrd ⊢ B ∈ V ∧ C ∈ W → B ≀ R ↾ A C ↔ ∃ u ∈ A u R B ∧ u R C