Theorem coep

Description: Composition with the membership relation. (Contributed by Scott Fenton, 18-Feb-2013)

	Ref	Expression
Hypotheses	coep.1	$$⊢A\in \mathrm{V}$$
	coep.2	$$⊢B\in \mathrm{V}$$
Assertion	coep	$$⊢A\left(\mathrm{E}\circ R\right)B\leftrightarrow \exists x\in BARx$$

Proof

Step	Hyp	Ref	Expression
1		coep.1	$$⊢A\in \mathrm{V}$$
2		coep.2	$$⊢B\in \mathrm{V}$$
3	2	epeli	$$⊢x\mathrm{E}B\leftrightarrow x\in B$$
4	3	anbi1ci	$$⊢\left(ARx\wedge x\mathrm{E}B\right)\leftrightarrow \left(x\in B\wedge ARx\right)$$
5	4	exbii	$$⊢\exists x\left(ARx\wedge x\mathrm{E}B\right)\leftrightarrow \exists x\left(x\in B\wedge ARx\right)$$
6	1 2	brco	$$⊢A\left(\mathrm{E}\circ R\right)B\leftrightarrow \exists x\left(ARx\wedge x\mathrm{E}B\right)$$
7		df-rex	$$⊢\exists x\in BARx\leftrightarrow \exists x\left(x\in B\wedge ARx\right)$$
8	5 6 7	3bitr4i	$$⊢A\left(\mathrm{E}\circ R\right)B\leftrightarrow \exists x\in BARx$$