# Metamath Proof Explorer

## Theorem oprabbid

Description: Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses oprabbid.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
oprabbid.2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
oprabbid.3 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
oprabbid.4 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
Assertion oprabbid ${⊢}{\phi }\to \left\{⟨⟨{x},{y}⟩,{z}⟩|{\psi }\right\}=\left\{⟨⟨{x},{y}⟩,{z}⟩|{\chi }\right\}$

### Proof

Step Hyp Ref Expression
1 oprabbid.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 oprabbid.2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 oprabbid.3 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
4 oprabbid.4 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
5 4 anbi2d ${⊢}{\phi }\to \left(\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\psi }\right)↔\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\chi }\right)\right)$
6 3 5 exbid ${⊢}{\phi }\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\psi }\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\chi }\right)\right)$
7 2 6 exbid ${⊢}{\phi }\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\psi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\chi }\right)\right)$
8 1 7 exbid ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\psi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\chi }\right)\right)$
9 8 abbidv ${⊢}{\phi }\to \left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\psi }\right)\right\}=\left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\chi }\right)\right\}$
10 df-oprab ${⊢}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\psi }\right\}=\left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\psi }\right)\right\}$
11 df-oprab ${⊢}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\chi }\right\}=\left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\chi }\right)\right\}$
12 9 10 11 3eqtr4g ${⊢}{\phi }\to \left\{⟨⟨{x},{y}⟩,{z}⟩|{\psi }\right\}=\left\{⟨⟨{x},{y}⟩,{z}⟩|{\chi }\right\}$