Theorem coepr

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

	Ref	Expression
Hypotheses	coep.1	|- A e. _V
	coep.2	|- B e. _V
Assertion	coepr	|- ( A ( R o. `' _E ) B <-> E. x e. A x R B )

Proof

Step	Hyp	Ref	Expression
1		coep.1	|- A e. _V
2		coep.2	|- B e. _V
3		vex	|- x e. _V
4	1 3	brcnv	|- ( A `' _E x <-> x _E A )
5	1	epeli	|- ( x _E A <-> x e. A )
6	4 5	bitri	|- ( A `' _E x <-> x e. A )
7	6	anbi1i	|- ( ( A `' _E x /\ x R B ) <-> ( x e. A /\ x R B ) )
8	7	exbii	|- ( E. x ( A `' _E x /\ x R B ) <-> E. x ( x e. A /\ x R B ) )
9	1 2	brco	|- ( A ( R o. `' _E ) B <-> E. x ( A `' _E x /\ x R B ) )
10		df-rex	|- ( E. x e. A x R B <-> E. x ( x e. A /\ x R B ) )
11	8 9 10	3bitr4i	|- ( A ( R o. `' _E ) B <-> E. x e. A x R B )