Metamath Proof Explorer

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∈V∧C∈W∧D∈X∧E∈Y→BC≀R⋉I↾ADE↔∃u∈Au=C∧uRB∧u=E∧uRD

Proof

Step Hyp Ref Expression
1 br1cossxrnres ⊢B∈V∧C∈W∧D∈X∧E∈Y→BC≀R⋉I↾ADE↔∃u∈AuIC∧uRB∧uIE∧uRD
2 ideq2 ⊢u∈V→uIC↔u=C
3 2 elv ⊢uIC↔u=C
4 3 anbi1i ⊢uIC∧uRB↔u=C∧uRB
5 ideq2 ⊢u∈V→uIE↔u=E
6 5 elv ⊢uIE↔u=E
7 6 anbi1i ⊢uIE∧uRD↔u=E∧uRD
8 4 7 anbi12i ⊢uIC∧uRB∧uIE∧uRD↔u=C∧uRB∧u=E∧uRD
9 8 rexbii ⊢∃u∈AuIC∧uRB∧uIE∧uRD↔∃u∈Au=C∧uRB∧u=E∧uRD
10 1 9 bitrdi ⊢B∈V∧C∈W∧D∈X∧E∈Y→BC≀R⋉I↾ADE↔∃u∈Au=C∧uRB∧u=E∧uRD