# Metamath Proof Explorer

## Theorem dropab2

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 dropab2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left\{⟨{z},{x}⟩|{\phi }\right\}=\left\{⟨{z},{y}⟩|{\phi }\right\}$

### Proof

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