Theorem brcog

Description: Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015)

	Ref	Expression
Assertion	brcog	|- ( ( A e. V /\ B e. W ) -> ( A ( C o. D ) B <-> E. x ( A D x /\ x C B ) ) )

Proof

Step	Hyp	Ref	Expression
1		breq1	|- ( y = A -> ( y D x <-> A D x ) )
2		breq2	|- ( z = B -> ( x C z <-> x C B ) )
3	1 2	bi2anan9	|- ( ( y = A /\ z = B ) -> ( ( y D x /\ x C z ) <-> ( A D x /\ x C B ) ) )
4	3	exbidv	|- ( ( y = A /\ z = B ) -> ( E. x ( y D x /\ x C z ) <-> E. x ( A D x /\ x C B ) ) )
5		df-co	|- ( C o. D ) = { <. y , z >. | E. x ( y D x /\ x C z ) }
6	4 5	brabga	|- ( ( A e. V /\ B e. W ) -> ( A ( C o. D ) B <-> E. x ( A D x /\ x C B ) ) )