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 = f p | f W p ψ τ
2rbropap.2 f = F p = P ψ χ
2rbropap.3 f = F p = P τ θ
Assertion 2rbropap φ F X P Y F M P F W P χ θ

Proof

Step Hyp Ref Expression
1 2rbropap.1 φ M = f p | f W p ψ τ
2 2rbropap.2 f = F p = P ψ χ
3 2rbropap.3 f = F p = P τ θ
4 3anass f W p ψ τ f W p ψ τ
5 4 opabbii f p | f W p ψ τ = f p | f W p ψ τ
6 1 5 eqtrdi φ M = f p | f W p ψ τ
7 2 3 anbi12d f = F p = P ψ τ χ θ
8 6 7 rbropap φ F X P Y F M P F W P χ θ
9 3anass F W P χ θ F W P χ θ
10 8 9 bitr4di φ F X P Y F M P F W P χ θ