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

Metamath Proof Explorer

Theorem rbropapd

Description: Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017)

Ref Expression
Hypotheses rbropapd.1 
|- ( ph -> M = { <. f , p >. | ( f W p /\ ps ) } )
rbropapd.2 
|- ( ( f = F /\ p = P ) -> ( ps <-> ch ) )
Assertion rbropapd 
|- ( ph -> ( ( F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ch ) ) ) )

Proof

Step Hyp Ref Expression
1 rbropapd.1 
 |-  ( ph -> M = { <. f , p >. | ( f W p /\ ps ) } )
2 rbropapd.2 
 |-  ( ( f = F /\ p = P ) -> ( ps <-> ch ) )
3 df-br 
 |-  ( F M P <-> <. F , P >. e. M )
4 1 eleq2d 
 |-  ( ph -> ( <. F , P >. e. M <-> <. F , P >. e. { <. f , p >. | ( f W p /\ ps ) } ) )
5 3 4 bitrid 
 |-  ( ph -> ( F M P <-> <. F , P >. e. { <. f , p >. | ( f W p /\ ps ) } ) )
6 breq12 
 |-  ( ( f = F /\ p = P ) -> ( f W p <-> F W P ) )
7 6 2 anbi12d 
 |-  ( ( f = F /\ p = P ) -> ( ( f W p /\ ps ) <-> ( F W P /\ ch ) ) )
8 7 opelopabga 
 |-  ( ( F e. X /\ P e. Y ) -> ( <. F , P >. e. { <. f , p >. | ( f W p /\ ps ) } <-> ( F W P /\ ch ) ) )
9 5 8 sylan9bb 
 |-  ( ( ph /\ ( F e. X /\ P e. Y ) ) -> ( F M P <-> ( F W P /\ ch ) ) )
10 9 ex 
 |-  ( ph -> ( ( F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ch ) ) ) )