# Metamath Proof Explorer

## Theorem inopab

Description: Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002)

Ref Expression
Assertion inopab ${⊢}\left\{⟨{x},{y}⟩|{\phi }\right\}\cap \left\{⟨{x},{y}⟩|{\psi }\right\}=\left\{⟨{x},{y}⟩|\left({\phi }\wedge {\psi }\right)\right\}$

### Proof

Step Hyp Ref Expression
1 relopab ${⊢}\mathrm{Rel}\left\{⟨{x},{y}⟩|{\phi }\right\}$
2 relin1 ${⊢}\mathrm{Rel}\left\{⟨{x},{y}⟩|{\phi }\right\}\to \mathrm{Rel}\left(\left\{⟨{x},{y}⟩|{\phi }\right\}\cap \left\{⟨{x},{y}⟩|{\psi }\right\}\right)$
3 1 2 ax-mp ${⊢}\mathrm{Rel}\left(\left\{⟨{x},{y}⟩|{\phi }\right\}\cap \left\{⟨{x},{y}⟩|{\psi }\right\}\right)$
4 relopab ${⊢}\mathrm{Rel}\left\{⟨{x},{y}⟩|\left({\phi }\wedge {\psi }\right)\right\}$
5 sban ${⊢}\left[{w}/{y}\right]\left(\left[{z}/{x}\right]{\phi }\wedge \left[{z}/{x}\right]{\psi }\right)↔\left(\left[{w}/{y}\right]\left[{z}/{x}\right]{\phi }\wedge \left[{w}/{y}\right]\left[{z}/{x}\right]{\psi }\right)$
6 sban ${⊢}\left[{z}/{x}\right]\left({\phi }\wedge {\psi }\right)↔\left(\left[{z}/{x}\right]{\phi }\wedge \left[{z}/{x}\right]{\psi }\right)$
7 6 sbbii ${⊢}\left[{w}/{y}\right]\left[{z}/{x}\right]\left({\phi }\wedge {\psi }\right)↔\left[{w}/{y}\right]\left(\left[{z}/{x}\right]{\phi }\wedge \left[{z}/{x}\right]{\psi }\right)$
8 opelopabsbALT ${⊢}⟨{z},{w}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}↔\left[{w}/{y}\right]\left[{z}/{x}\right]{\phi }$
9 opelopabsbALT ${⊢}⟨{z},{w}⟩\in \left\{⟨{x},{y}⟩|{\psi }\right\}↔\left[{w}/{y}\right]\left[{z}/{x}\right]{\psi }$
10 8 9 anbi12i ${⊢}\left(⟨{z},{w}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}\wedge ⟨{z},{w}⟩\in \left\{⟨{x},{y}⟩|{\psi }\right\}\right)↔\left(\left[{w}/{y}\right]\left[{z}/{x}\right]{\phi }\wedge \left[{w}/{y}\right]\left[{z}/{x}\right]{\psi }\right)$
11 5 7 10 3bitr4ri ${⊢}\left(⟨{z},{w}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}\wedge ⟨{z},{w}⟩\in \left\{⟨{x},{y}⟩|{\psi }\right\}\right)↔\left[{w}/{y}\right]\left[{z}/{x}\right]\left({\phi }\wedge {\psi }\right)$
12 elin ${⊢}⟨{z},{w}⟩\in \left(\left\{⟨{x},{y}⟩|{\phi }\right\}\cap \left\{⟨{x},{y}⟩|{\psi }\right\}\right)↔\left(⟨{z},{w}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}\wedge ⟨{z},{w}⟩\in \left\{⟨{x},{y}⟩|{\psi }\right\}\right)$
13 opelopabsbALT ${⊢}⟨{z},{w}⟩\in \left\{⟨{x},{y}⟩|\left({\phi }\wedge {\psi }\right)\right\}↔\left[{w}/{y}\right]\left[{z}/{x}\right]\left({\phi }\wedge {\psi }\right)$
14 11 12 13 3bitr4i ${⊢}⟨{z},{w}⟩\in \left(\left\{⟨{x},{y}⟩|{\phi }\right\}\cap \left\{⟨{x},{y}⟩|{\psi }\right\}\right)↔⟨{z},{w}⟩\in \left\{⟨{x},{y}⟩|\left({\phi }\wedge {\psi }\right)\right\}$
15 3 4 14 eqrelriiv ${⊢}\left\{⟨{x},{y}⟩|{\phi }\right\}\cap \left\{⟨{x},{y}⟩|{\psi }\right\}=\left\{⟨{x},{y}⟩|\left({\phi }\wedge {\psi }\right)\right\}$