Theorem 2rbropap

Description: Properties of a pair in a restricted binary relation M expressed as an ordered-pair class abstraction: M is the binary relation W restricted by the conditions ps and ta . (Contributed by AV, 31-Jan-2021)

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

Proof

Step	Hyp	Ref	Expression
1		2rbropap.1	|- ( ph -> M = { <. f , p >. | ( f W p /\ ps /\ ta ) } )
2		2rbropap.2	|- ( ( f = F /\ p = P ) -> ( ps <-> ch ) )
3		2rbropap.3	|- ( ( f = F /\ p = P ) -> ( ta <-> th ) )
4		3anass	|- ( ( f W p /\ ps /\ ta ) <-> ( f W p /\ ( ps /\ ta ) ) )
5	4	opabbii	|- { <. f , p >. | ( f W p /\ ps /\ ta ) } = { <. f , p >. | ( f W p /\ ( ps /\ ta ) ) }
6	1 5	eqtrdi	|- ( ph -> M = { <. f , p >. | ( f W p /\ ( ps /\ ta ) ) } )
7	2 3	anbi12d	|- ( ( f = F /\ p = P ) -> ( ( ps /\ ta ) <-> ( ch /\ th ) ) )
8	6 7	rbropap	|- ( ( ph /\ F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ( ch /\ th ) ) ) )
9		3anass	|- ( ( F W P /\ ch /\ th ) <-> ( F W P /\ ( ch /\ th ) ) )
10	8 9	bitr4di	|- ( ( ph /\ F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ch /\ th ) ) )