# Metamath Proof Explorer

## Theorem shftdm

Description: Domain of a relation shifted by A . The set on the right is more commonly notated as ( dom F + A ) (meaning add A to every element of dom F ). (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypothesis shftfval.1 ${⊢}{F}\in \mathrm{V}$
Assertion shftdm ${⊢}{A}\in ℂ\to \mathrm{dom}\left({F}\mathrm{shift}{A}\right)=\left\{{x}\in ℂ|{x}-{A}\in \mathrm{dom}{F}\right\}$

### Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 1 shftfval ${⊢}{A}\in ℂ\to {F}\mathrm{shift}{A}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
3 2 dmeqd ${⊢}{A}\in ℂ\to \mathrm{dom}\left({F}\mathrm{shift}{A}\right)=\mathrm{dom}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
4 19.42v ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)↔\left({x}\in ℂ\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}-{A}\right){F}{y}\right)$
5 ovex ${⊢}{x}-{A}\in \mathrm{V}$
6 5 eldm ${⊢}{x}-{A}\in \mathrm{dom}{F}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}-{A}\right){F}{y}$
7 6 anbi2i ${⊢}\left({x}\in ℂ\wedge {x}-{A}\in \mathrm{dom}{F}\right)↔\left({x}\in ℂ\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}-{A}\right){F}{y}\right)$
8 4 7 bitr4i ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)↔\left({x}\in ℂ\wedge {x}-{A}\in \mathrm{dom}{F}\right)$
9 8 abbii ${⊢}\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}=\left\{{x}|\left({x}\in ℂ\wedge {x}-{A}\in \mathrm{dom}{F}\right)\right\}$
10 dmopab ${⊢}\mathrm{dom}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
11 df-rab ${⊢}\left\{{x}\in ℂ|{x}-{A}\in \mathrm{dom}{F}\right\}=\left\{{x}|\left({x}\in ℂ\wedge {x}-{A}\in \mathrm{dom}{F}\right)\right\}$
12 9 10 11 3eqtr4i ${⊢}\mathrm{dom}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}=\left\{{x}\in ℂ|{x}-{A}\in \mathrm{dom}{F}\right\}$
13 3 12 eqtrdi ${⊢}{A}\in ℂ\to \mathrm{dom}\left({F}\mathrm{shift}{A}\right)=\left\{{x}\in ℂ|{x}-{A}\in \mathrm{dom}{F}\right\}$