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

Metamath Proof Explorer

Theorem brcogw

Description: Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018)

Ref Expression
Assertion brcogw 
|- ( ( ( A e. V /\ B e. W /\ X e. Z ) /\ ( A D X /\ X C B ) ) -> A ( C o. D ) B )

Proof

Step Hyp Ref Expression
1 3simpa 
 |-  ( ( A e. V /\ B e. W /\ X e. Z ) -> ( A e. V /\ B e. W ) )
2 breq2 
 |-  ( x = X -> ( A D x <-> A D X ) )
3 breq1 
 |-  ( x = X -> ( x C B <-> X C B ) )
4 2 3 anbi12d 
 |-  ( x = X -> ( ( A D x /\ x C B ) <-> ( A D X /\ X C B ) ) )
5 4 spcegv 
 |-  ( X e. Z -> ( ( A D X /\ X C B ) -> E. x ( A D x /\ x C B ) ) )
6 5 imp 
 |-  ( ( X e. Z /\ ( A D X /\ X C B ) ) -> E. x ( A D x /\ x C B ) )
7 6 3ad2antl3 
 |-  ( ( ( A e. V /\ B e. W /\ X e. Z ) /\ ( A D X /\ X C B ) ) -> E. x ( A D x /\ x C B ) )
8 brcog 
 |-  ( ( A e. V /\ B e. W ) -> ( A ( C o. D ) B <-> E. x ( A D x /\ x C B ) ) )
9 8 biimpar 
 |-  ( ( ( A e. V /\ B e. W ) /\ E. x ( A D x /\ x C B ) ) -> A ( C o. D ) B )
10 1 7 9 syl2an2r 
 |-  ( ( ( A e. V /\ B e. W /\ X e. Z ) /\ ( A D X /\ X C B ) ) -> A ( C o. D ) B )