Theorem rbropap

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 condition ps . (Contributed by AV, 31-Jan-2021)

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