# Metamath Proof Explorer

## Theorem dropab1

Description: Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion dropab1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left\{⟨{x},{z}⟩|{\phi }\right\}=\left\{⟨{y},{z}⟩|{\phi }\right\}$

### Proof

Step Hyp Ref Expression
1 opeq1 ${⊢}{x}={y}\to ⟨{x},{z}⟩=⟨{y},{z}⟩$
2 1 sps ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to ⟨{x},{z}⟩=⟨{y},{z}⟩$
3 2 eqeq2d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({w}=⟨{x},{z}⟩↔{w}=⟨{y},{z}⟩\right)$
4 3 anbi1d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\left({w}=⟨{x},{z}⟩\wedge {\phi }\right)↔\left({w}=⟨{y},{z}⟩\wedge {\phi }\right)\right)$
5 4 drex2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{z}⟩\wedge {\phi }\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{y},{z}⟩\wedge {\phi }\right)\right)$
6 5 drex1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{z}⟩\wedge {\phi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{y},{z}⟩\wedge {\phi }\right)\right)$
7 6 abbidv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{z}⟩\wedge {\phi }\right)\right\}=\left\{{w}|\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{y},{z}⟩\wedge {\phi }\right)\right\}$
8 df-opab ${⊢}\left\{⟨{x},{z}⟩|{\phi }\right\}=\left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{z}⟩\wedge {\phi }\right)\right\}$
9 df-opab ${⊢}\left\{⟨{y},{z}⟩|{\phi }\right\}=\left\{{w}|\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{y},{z}⟩\wedge {\phi }\right)\right\}$
10 7 8 9 3eqtr4g ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left\{⟨{x},{z}⟩|{\phi }\right\}=\left\{⟨{y},{z}⟩|{\phi }\right\}$