Theorem coep

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

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

Proof

Step	Hyp	Ref	Expression
1		coep.1	|- A e. _V
2		coep.2	|- B e. _V
3	2	epeli	|- ( x _E B <-> x e. B )
4	3	anbi1ci	|- ( ( A R x /\ x _E B ) <-> ( x e. B /\ A R x ) )
5	4	exbii	|- ( E. x ( A R x /\ x _E B ) <-> E. x ( x e. B /\ A R x ) )
6	1 2	brco	|- ( A ( _E o. R ) B <-> E. x ( A R x /\ x _E B ) )
7		df-rex	|- ( E. x e. B A R x <-> E. x ( x e. B /\ A R x ) )
8	5 6 7	3bitr4i	|- ( A ( _E o. R ) B <-> E. x e. B A R x )