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