# Metamath Proof Explorer

## Theorem rbropapd

Description: Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017)

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 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)$

### 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 df-br ${⊢}{F}{M}{P}↔⟨{F},{P}⟩\in {M}$
4 1 eleq2d ${⊢}{\phi }\to \left(⟨{F},{P}⟩\in {M}↔⟨{F},{P}⟩\in \left\{⟨{f},{p}⟩|\left({f}{W}{p}\wedge {\psi }\right)\right\}\right)$
5 3 4 syl5bb ${⊢}{\phi }\to \left({F}{M}{P}↔⟨{F},{P}⟩\in \left\{⟨{f},{p}⟩|\left({f}{W}{p}\wedge {\psi }\right)\right\}\right)$
6 breq12 ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left({f}{W}{p}↔{F}{W}{P}\right)$
7 6 2 anbi12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left(\left({f}{W}{p}\wedge {\psi }\right)↔\left({F}{W}{P}\wedge {\chi }\right)\right)$
8 7 opelopabga ${⊢}\left({F}\in {X}\wedge {P}\in {Y}\right)\to \left(⟨{F},{P}⟩\in \left\{⟨{f},{p}⟩|\left({f}{W}{p}\wedge {\psi }\right)\right\}↔\left({F}{W}{P}\wedge {\chi }\right)\right)$
9 5 8 sylan9bb ${⊢}\left({\phi }\wedge \left({F}\in {X}\wedge {P}\in {Y}\right)\right)\to \left({F}{M}{P}↔\left({F}{W}{P}\wedge {\chi }\right)\right)$
10 9 ex ${⊢}{\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)$