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 e. V /\ C e. W ) -> ( B ,~ ( R i^i ( _I |` A ) ) C <-> E. u e. A ( ( u = B /\ u R B ) /\ ( u = C /\ u R C ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		br1cossinres	|- ( ( B e. V /\ C e. W ) -> ( B ,~ ( R i^i ( _I |` A ) ) C <-> E. u e. A ( ( u _I B /\ u R B ) /\ ( u _I C /\ u R C ) ) ) )
2		ideq2	|- ( u e. _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 e. _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	|- ( E. u e. A ( ( u _I B /\ u R B ) /\ ( u _I C /\ u R C ) ) <-> E. u e. A ( ( u = B /\ u R B ) /\ ( u = C /\ u R C ) ) )
10	1 9	bitrdi	|- ( ( B e. V /\ C e. W ) -> ( B ,~ ( R i^i ( _I |` A ) ) C <-> E. u e. A ( ( u = B /\ u R B ) /\ ( u = C /\ u R C ) ) ) )