This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )