# Metamath Proof Explorer

## Theorem opbrop

Description: Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995)

Ref Expression
Hypotheses opbrop.1 ${⊢}\left(\left({z}={A}\wedge {w}={B}\right)\wedge \left({v}={C}\wedge {u}={D}\right)\right)\to \left({\phi }↔{\psi }\right)$
opbrop.2 ${⊢}{R}=\left\{⟨{x},{y}⟩|\left(\left({x}\in \left({S}×{S}\right)\wedge {y}\in \left({S}×{S}\right)\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)\right\}$
Assertion opbrop ${⊢}\left(\left({A}\in {S}\wedge {B}\in {S}\right)\wedge \left({C}\in {S}\wedge {D}\in {S}\right)\right)\to \left(⟨{A},{B}⟩{R}⟨{C},{D}⟩↔{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 opbrop.1 ${⊢}\left(\left({z}={A}\wedge {w}={B}\right)\wedge \left({v}={C}\wedge {u}={D}\right)\right)\to \left({\phi }↔{\psi }\right)$
2 opbrop.2 ${⊢}{R}=\left\{⟨{x},{y}⟩|\left(\left({x}\in \left({S}×{S}\right)\wedge {y}\in \left({S}×{S}\right)\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)\right\}$
3 opelxpi ${⊢}\left({A}\in {S}\wedge {B}\in {S}\right)\to ⟨{A},{B}⟩\in \left({S}×{S}\right)$
4 opelxpi ${⊢}\left({C}\in {S}\wedge {D}\in {S}\right)\to ⟨{C},{D}⟩\in \left({S}×{S}\right)$
5 3 4 anim12i ${⊢}\left(\left({A}\in {S}\wedge {B}\in {S}\right)\wedge \left({C}\in {S}\wedge {D}\in {S}\right)\right)\to \left(⟨{A},{B}⟩\in \left({S}×{S}\right)\wedge ⟨{C},{D}⟩\in \left({S}×{S}\right)\right)$
6 opex ${⊢}⟨{A},{B}⟩\in \mathrm{V}$
7 opex ${⊢}⟨{C},{D}⟩\in \mathrm{V}$
8 eleq1 ${⊢}{x}=⟨{A},{B}⟩\to \left({x}\in \left({S}×{S}\right)↔⟨{A},{B}⟩\in \left({S}×{S}\right)\right)$
9 8 anbi1d ${⊢}{x}=⟨{A},{B}⟩\to \left(\left({x}\in \left({S}×{S}\right)\wedge {y}\in \left({S}×{S}\right)\right)↔\left(⟨{A},{B}⟩\in \left({S}×{S}\right)\wedge {y}\in \left({S}×{S}\right)\right)\right)$
10 eqeq1 ${⊢}{x}=⟨{A},{B}⟩\to \left({x}=⟨{z},{w}⟩↔⟨{A},{B}⟩=⟨{z},{w}⟩\right)$
11 10 anbi1d ${⊢}{x}=⟨{A},{B}⟩\to \left(\left({x}=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)↔\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\right)$
12 11 anbi1d ${⊢}{x}=⟨{A},{B}⟩\to \left(\left(\left({x}=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\wedge {\phi }\right)↔\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)$
13 12 4exbidv ${⊢}{x}=⟨{A},{B}⟩\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\wedge {\phi }\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)$
14 9 13 anbi12d ${⊢}{x}=⟨{A},{B}⟩\to \left(\left(\left({x}\in \left({S}×{S}\right)\wedge {y}\in \left({S}×{S}\right)\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)↔\left(\left(⟨{A},{B}⟩\in \left({S}×{S}\right)\wedge {y}\in \left({S}×{S}\right)\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)\right)$
15 eleq1 ${⊢}{y}=⟨{C},{D}⟩\to \left({y}\in \left({S}×{S}\right)↔⟨{C},{D}⟩\in \left({S}×{S}\right)\right)$
16 15 anbi2d ${⊢}{y}=⟨{C},{D}⟩\to \left(\left(⟨{A},{B}⟩\in \left({S}×{S}\right)\wedge {y}\in \left({S}×{S}\right)\right)↔\left(⟨{A},{B}⟩\in \left({S}×{S}\right)\wedge ⟨{C},{D}⟩\in \left({S}×{S}\right)\right)\right)$
17 eqeq1 ${⊢}{y}=⟨{C},{D}⟩\to \left({y}=⟨{v},{u}⟩↔⟨{C},{D}⟩=⟨{v},{u}⟩\right)$
18 17 anbi2d ${⊢}{y}=⟨{C},{D}⟩\to \left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)↔\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge ⟨{C},{D}⟩=⟨{v},{u}⟩\right)\right)$
19 18 anbi1d ${⊢}{y}=⟨{C},{D}⟩\to \left(\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\wedge {\phi }\right)↔\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge ⟨{C},{D}⟩=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)$
20 19 4exbidv ${⊢}{y}=⟨{C},{D}⟩\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\wedge {\phi }\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge ⟨{C},{D}⟩=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)$
21 16 20 anbi12d ${⊢}{y}=⟨{C},{D}⟩\to \left(\left(\left(⟨{A},{B}⟩\in \left({S}×{S}\right)\wedge {y}\in \left({S}×{S}\right)\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge {y}=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)↔\left(\left(⟨{A},{B}⟩\in \left({S}×{S}\right)\wedge ⟨{C},{D}⟩\in \left({S}×{S}\right)\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge ⟨{C},{D}⟩=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)\right)$
22 6 7 14 21 2 brab ${⊢}⟨{A},{B}⟩{R}⟨{C},{D}⟩↔\left(\left(⟨{A},{B}⟩\in \left({S}×{S}\right)\wedge ⟨{C},{D}⟩\in \left({S}×{S}\right)\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge ⟨{C},{D}⟩=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)$
23 1 copsex4g ${⊢}\left(\left({A}\in {S}\wedge {B}\in {S}\right)\wedge \left({C}\in {S}\wedge {D}\in {S}\right)\right)\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge ⟨{C},{D}⟩=⟨{v},{u}⟩\right)\wedge {\phi }\right)↔{\psi }\right)$
24 23 anbi2d ${⊢}\left(\left({A}\in {S}\wedge {B}\in {S}\right)\wedge \left({C}\in {S}\wedge {D}\in {S}\right)\right)\to \left(\left(\left(⟨{A},{B}⟩\in \left({S}×{S}\right)\wedge ⟨{C},{D}⟩\in \left({S}×{S}\right)\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩=⟨{z},{w}⟩\wedge ⟨{C},{D}⟩=⟨{v},{u}⟩\right)\wedge {\phi }\right)\right)↔\left(\left(⟨{A},{B}⟩\in \left({S}×{S}\right)\wedge ⟨{C},{D}⟩\in \left({S}×{S}\right)\right)\wedge {\psi }\right)\right)$
25 22 24 syl5bb ${⊢}\left(\left({A}\in {S}\wedge {B}\in {S}\right)\wedge \left({C}\in {S}\wedge {D}\in {S}\right)\right)\to \left(⟨{A},{B}⟩{R}⟨{C},{D}⟩↔\left(\left(⟨{A},{B}⟩\in \left({S}×{S}\right)\wedge ⟨{C},{D}⟩\in \left({S}×{S}\right)\right)\wedge {\psi }\right)\right)$
26 5 25 mpbirand ${⊢}\left(\left({A}\in {S}\wedge {B}\in {S}\right)\wedge \left({C}\in {S}\wedge {D}\in {S}\right)\right)\to \left(⟨{A},{B}⟩{R}⟨{C},{D}⟩↔{\psi }\right)$