# 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 ${⊢}{\phi }\to {M}=\left\{⟨{f},{p}⟩|\left({f}{W}{p}\wedge {\psi }\wedge {\tau }\right)\right\}$
2rbropap.2 ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left({\psi }↔{\chi }\right)$
2rbropap.3 ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left({\tau }↔{\theta }\right)$
Assertion 2rbropap ${⊢}\left({\phi }\wedge {F}\in {X}\wedge {P}\in {Y}\right)\to \left({F}{M}{P}↔\left({F}{W}{P}\wedge {\chi }\wedge {\theta }\right)\right)$

### Proof

Step Hyp Ref Expression
1 2rbropap.1 ${⊢}{\phi }\to {M}=\left\{⟨{f},{p}⟩|\left({f}{W}{p}\wedge {\psi }\wedge {\tau }\right)\right\}$
2 2rbropap.2 ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left({\psi }↔{\chi }\right)$
3 2rbropap.3 ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left({\tau }↔{\theta }\right)$
4 3anass ${⊢}\left({f}{W}{p}\wedge {\psi }\wedge {\tau }\right)↔\left({f}{W}{p}\wedge \left({\psi }\wedge {\tau }\right)\right)$
5 4 opabbii ${⊢}\left\{⟨{f},{p}⟩|\left({f}{W}{p}\wedge {\psi }\wedge {\tau }\right)\right\}=\left\{⟨{f},{p}⟩|\left({f}{W}{p}\wedge \left({\psi }\wedge {\tau }\right)\right)\right\}$
6 1 5 syl6eq ${⊢}{\phi }\to {M}=\left\{⟨{f},{p}⟩|\left({f}{W}{p}\wedge \left({\psi }\wedge {\tau }\right)\right)\right\}$
7 2 3 anbi12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left(\left({\psi }\wedge {\tau }\right)↔\left({\chi }\wedge {\theta }\right)\right)$
8 6 7 rbropap ${⊢}\left({\phi }\wedge {F}\in {X}\wedge {P}\in {Y}\right)\to \left({F}{M}{P}↔\left({F}{W}{P}\wedge \left({\chi }\wedge {\theta }\right)\right)\right)$
9 3anass ${⊢}\left({F}{W}{P}\wedge {\chi }\wedge {\theta }\right)↔\left({F}{W}{P}\wedge \left({\chi }\wedge {\theta }\right)\right)$
10 8 9 syl6bbr ${⊢}\left({\phi }\wedge {F}\in {X}\wedge {P}\in {Y}\right)\to \left({F}{M}{P}↔\left({F}{W}{P}\wedge {\chi }\wedge {\theta }\right)\right)$