# Metamath Proof Explorer

## Theorem brcog

Description: Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015)

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

### Proof

Step Hyp Ref Expression
1 breq1 ${⊢}{y}={A}\to \left({y}{D}{x}↔{A}{D}{x}\right)$
2 breq2 ${⊢}{z}={B}\to \left({x}{C}{z}↔{x}{C}{B}\right)$
3 1 2 bi2anan9 ${⊢}\left({y}={A}\wedge {z}={B}\right)\to \left(\left({y}{D}{x}\wedge {x}{C}{z}\right)↔\left({A}{D}{x}\wedge {x}{C}{B}\right)\right)$
4 3 exbidv ${⊢}\left({y}={A}\wedge {z}={B}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{D}{x}\wedge {x}{C}{z}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({A}{D}{x}\wedge {x}{C}{B}\right)\right)$
5 df-co ${⊢}{C}\circ {D}=\left\{⟨{y},{z}⟩|\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{D}{x}\wedge {x}{C}{z}\right)\right\}$
6 4 5 brabga ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({A}\left({C}\circ {D}\right){B}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({A}{D}{x}\wedge {x}{C}{B}\right)\right)$