Theorem opelco2g

Description: Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997) (Revised by Mario Carneiro, 24-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		brcog	|- ( ( A e. V /\ B e. W ) -> ( A ( C o. D ) B <-> E. x ( A D x /\ x C B ) ) )
2		df-br	|- ( A ( C o. D ) B <-> <. A , B >. e. ( C o. D ) )
3		df-br	|- ( A D x <-> <. A , x >. e. D )
4		df-br	|- ( x C B <-> <. x , B >. e. C )
5	3 4	anbi12i	|- ( ( A D x /\ x C B ) <-> ( <. A , x >. e. D /\ <. x , B >. e. C ) )
6	5	exbii	|- ( E. x ( A D x /\ x C B ) <-> E. x ( <. A , x >. e. D /\ <. x , B >. e. C ) )
7	1 2 6	3bitr3g	|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. ( C o. D ) <-> E. x ( <. A , x >. e. D /\ <. x , B >. e. C ) ) )