Metamath Proof Explorer

Theorem br1cossinidres

Description: B and C are cosets by an intersection with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion br1cossinidres ⊢B∈V∧C∈W→B≀R∩I↾AC↔∃u∈Au=B∧uRB∧u=C∧uRC

Proof

Step Hyp Ref Expression
1 br1cossinres ⊢B∈V∧C∈W→B≀R∩I↾AC↔∃u∈AuIB∧uRB∧uIC∧uRC
2 ideq2 ⊢u∈V→uIB↔u=B
3 2 elv ⊢uIB↔u=B
4 3 anbi1i ⊢uIB∧uRB↔u=B∧uRB
5 ideq2 ⊢u∈V→uIC↔u=C
6 5 elv ⊢uIC↔u=C
7 6 anbi1i ⊢uIC∧uRC↔u=C∧uRC
8 4 7 anbi12i ⊢uIB∧uRB∧uIC∧uRC↔u=B∧uRB∧u=C∧uRC
9 8 rexbii ⊢∃u∈AuIB∧uRB∧uIC∧uRC↔∃u∈Au=B∧uRB∧u=C∧uRC
10 1 9 bitrdi ⊢B∈V∧C∈W→B≀R∩I↾AC↔∃u∈Au=B∧uRB∧u=C∧uRC