Theorem br1cossxrnidres

Description: <. B , C >. and <. D , E >. are cosets by a range Cartesian product with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021)

	Ref	Expression
Assertion	br1cossxrnidres	|- ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( _I |` A ) ) <. D , E >. <-> E. u e. A ( ( u = C /\ u R B ) /\ ( u = E /\ u R D ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		br1cossxrnres	|- ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( _I |` A ) ) <. D , E >. <-> E. u e. A ( ( u _I C /\ u R B ) /\ ( u _I E /\ u R D ) ) ) )
2		ideq2	|- ( u e. _V -> ( u _I C <-> u = C ) )
3	2	elv	|- ( u _I C <-> u = C )
4	3	anbi1i	|- ( ( u _I C /\ u R B ) <-> ( u = C /\ u R B ) )
5		ideq2	|- ( u e. _V -> ( u _I E <-> u = E ) )
6	5	elv	|- ( u _I E <-> u = E )
7	6	anbi1i	|- ( ( u _I E /\ u R D ) <-> ( u = E /\ u R D ) )
8	4 7	anbi12i	|- ( ( ( u _I C /\ u R B ) /\ ( u _I E /\ u R D ) ) <-> ( ( u = C /\ u R B ) /\ ( u = E /\ u R D ) ) )
9	8	rexbii	|- ( E. u e. A ( ( u _I C /\ u R B ) /\ ( u _I E /\ u R D ) ) <-> E. u e. A ( ( u = C /\ u R B ) /\ ( u = E /\ u R D ) ) )
10	1 9	bitrdi	|- ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( _I |` A ) ) <. D , E >. <-> E. u e. A ( ( u = C /\ u R B ) /\ ( u = E /\ u R D ) ) ) )