Metamath Proof Explorer


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 φM=fp|fWpψτ
2rbropap.2 f=Fp=Pψχ
2rbropap.3 f=Fp=Pτθ
Assertion 2rbropap φFXPYFMPFWPχθ

Proof

Step Hyp Ref Expression
1 2rbropap.1 φM=fp|fWpψτ
2 2rbropap.2 f=Fp=Pψχ
3 2rbropap.3 f=Fp=Pτθ
4 3anass fWpψτfWpψτ
5 4 opabbii fp|fWpψτ=fp|fWpψτ
6 1 5 eqtrdi φM=fp|fWpψτ
7 2 3 anbi12d f=Fp=Pψτχθ
8 6 7 rbropap φFXPYFMPFWPχθ
9 3anass FWPχθFWPχθ
10 8 9 bitr4di φFXPYFMPFWPχθ