Metamath Proof Explorer

Theorem br1cossres2

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

Ref Expression
Assertion br1cossres2 ⊢B∈V∧C∈W→B≀R↾AC↔∃x∈AB∈xR∧C∈xR

Proof

Step Hyp Ref Expression
1 br1cossres ⊢B∈V∧C∈W→B≀R↾AC↔∃x∈AxRB∧xRC
2 exanres3 ⊢B∈V∧C∈W→∃x∈AB∈xR∧C∈xR↔∃x∈AxRB∧xRC
3 1 2 bitr4d ⊢B∈V∧C∈W→B≀R↾AC↔∃x∈AB∈xR∧C∈xR