Theorem coepr

Description: Composition with the converse 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	coepr	$$⊢A\left(R\circ {\mathrm{E}}^{-1}\right)B\leftrightarrow \exists x\in AxRB$$

Proof

Step	Hyp	Ref	Expression
1		coep.1	$$⊢A\in \mathrm{V}$$
2		coep.2	$$⊢B\in \mathrm{V}$$
3		vex	$$⊢x\in \mathrm{V}$$
4	1 3	brcnv	$$⊢A{\mathrm{E}}^{-1}x\leftrightarrow x\mathrm{E}A$$
5	1	epeli	$$⊢x\mathrm{E}A\leftrightarrow x\in A$$
6	4 5	bitri	$$⊢A{\mathrm{E}}^{-1}x\leftrightarrow x\in A$$
7	6	anbi1i	$$⊢\left(A{\mathrm{E}}^{-1}x\wedge xRB\right)\leftrightarrow \left(x\in A\wedge xRB\right)$$
8	7	exbii	$$⊢\exists x\left(A{\mathrm{E}}^{-1}x\wedge xRB\right)\leftrightarrow \exists x\left(x\in A\wedge xRB\right)$$
9	1 2	brco	$$⊢A\left(R\circ {\mathrm{E}}^{-1}\right)B\leftrightarrow \exists x\left(A{\mathrm{E}}^{-1}x\wedge xRB\right)$$
10		df-rex	$$⊢\exists x\in AxRB\leftrightarrow \exists x\left(x\in A\wedge xRB\right)$$
11	8 9 10	3bitr4i	$$⊢A\left(R\circ {\mathrm{E}}^{-1}\right)B\leftrightarrow \exists x\in AxRB$$