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 A C u A u = B u R B u = C u R C

Proof

Step Hyp Ref Expression
1 br1cossinres B V C W B R I A C u A u I B u R B u I C u R C
2 ideq2 u V u I B u = B
3 2 elv u I B u = B
4 3 anbi1i u I B u R B u = B u R B
5 ideq2 u V u I C u = C
6 5 elv u I C u = C
7 6 anbi1i u I C u R C u = C u R C
8 4 7 anbi12i u I B u R B u I C u R C u = B u R B u = C u R C
9 8 rexbii u A u I B u R B u I C u R C u A u = B u R B u = C u R C
10 1 9 bitrdi B V C W B R I A C u A u = B u R B u = C u R C