# Metamath Proof Explorer

## Theorem brcoels

Description: B and C are coelements : a binary relation. (Contributed by Peter Mazsa, 14-Jan-2020) (Revised by Peter Mazsa, 5-Oct-2021)

Ref Expression
Assertion brcoels ${⊢}\left({B}\in {V}\wedge {C}\in {W}\right)\to \left({B}\sim {A}{C}↔\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\in {u}\wedge {C}\in {u}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eleq1 ${⊢}{x}={B}\to \left({x}\in {u}↔{B}\in {u}\right)$
2 eleq1 ${⊢}{y}={C}\to \left({y}\in {u}↔{C}\in {u}\right)$
3 1 2 bi2anan9 ${⊢}\left({x}={B}\wedge {y}={C}\right)\to \left(\left({x}\in {u}\wedge {y}\in {u}\right)↔\left({B}\in {u}\wedge {C}\in {u}\right)\right)$
4 3 rexbidv ${⊢}\left({x}={B}\wedge {y}={C}\right)\to \left(\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {u}\wedge {y}\in {u}\right)↔\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\in {u}\wedge {C}\in {u}\right)\right)$
5 dfcoels ${⊢}\sim {A}=\left\{⟨{x},{y}⟩|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {u}\wedge {y}\in {u}\right)\right\}$
6 4 5 brabga ${⊢}\left({B}\in {V}\wedge {C}\in {W}\right)\to \left({B}\sim {A}{C}↔\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\in {u}\wedge {C}\in {u}\right)\right)$