Theorem brco

Description: Binary relation on a composition. (Contributed by NM, 21-Sep-2004) (Revised by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	opelco.1	$$⊢A\in \mathrm{V}$$
	opelco.2	$$⊢B\in \mathrm{V}$$
Assertion	brco	$$⊢A\left(C\circ D\right)B\leftrightarrow \exists x\left(ADx\wedge xCB\right)$$

Proof

Step	Hyp	Ref	Expression
1		opelco.1	$$⊢A\in \mathrm{V}$$
2		opelco.2	$$⊢B\in \mathrm{V}$$
3		brcog	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(A\left(C\circ D\right)B\leftrightarrow \exists x\left(ADx\wedge xCB\right)\right)$$
4	1 2 3	mp2an	$$⊢A\left(C\circ D\right)B\leftrightarrow \exists x\left(ADx\wedge xCB\right)$$