# Metamath Proof Explorer

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

### Proof

Step Hyp Ref Expression
1 rbropapd.1 ${⊢}{\phi }\to {M}=\left\{⟨{f},{p}⟩|\left({f}{W}{p}\wedge {\psi }\right)\right\}$
2 rbropapd.2 ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left({\psi }↔{\chi }\right)$
3 1 2 rbropapd ${⊢}{\phi }\to \left(\left({F}\in {X}\wedge {P}\in {Y}\right)\to \left({F}{M}{P}↔\left({F}{W}{P}\wedge {\chi }\right)\right)\right)$
4 3 3impib ${⊢}\left({\phi }\wedge {F}\in {X}\wedge {P}\in {Y}\right)\to \left({F}{M}{P}↔\left({F}{W}{P}\wedge {\chi }\right)\right)$