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↾AC↔∃u∈AuRB∧uRC

Proof

Step Hyp Ref Expression
1 brcoss ⊢B∈V∧C∈W→B≀R↾AC↔∃uuR↾AB∧uR↾AC
2 exanres ⊢B∈V∧C∈W→∃uuR↾AB∧uR↾AC↔∃u∈AuRB∧uRC
3 1 2 bitrd ⊢B∈V∧C∈W→B≀R↾AC↔∃u∈AuRB∧uRC