# Metamath Proof Explorer

## Theorem shftlem

Description: Two ways to write a shifted set ( B + A ) . (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion shftlem ${⊢}\left({A}\in ℂ\wedge {B}\subseteq ℂ\right)\to \left\{{x}\in ℂ|{x}-{A}\in {B}\right\}=\left\{{x}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}={y}+{A}\right\}$

### Proof

Step Hyp Ref Expression
1 df-rab ${⊢}\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}=\left\{{x}|\left({x}\in ℂ\wedge {x}-{A}\in {B}\right)\right\}$
2 npcan ${⊢}\left({x}\in ℂ\wedge {A}\in ℂ\right)\to {x}-{A}+{A}={x}$
3 2 ancoms ${⊢}\left({A}\in ℂ\wedge {x}\in ℂ\right)\to {x}-{A}+{A}={x}$
4 3 eqcomd ${⊢}\left({A}\in ℂ\wedge {x}\in ℂ\right)\to {x}={x}-{A}+{A}$
5 oveq1 ${⊢}{y}={x}-{A}\to {y}+{A}={x}-{A}+{A}$
6 5 rspceeqv ${⊢}\left({x}-{A}\in {B}\wedge {x}={x}-{A}+{A}\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}={y}+{A}$
7 6 expcom ${⊢}{x}={x}-{A}+{A}\to \left({x}-{A}\in {B}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}={y}+{A}\right)$
8 4 7 syl ${⊢}\left({A}\in ℂ\wedge {x}\in ℂ\right)\to \left({x}-{A}\in {B}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}={y}+{A}\right)$
9 8 expimpd ${⊢}{A}\in ℂ\to \left(\left({x}\in ℂ\wedge {x}-{A}\in {B}\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}={y}+{A}\right)$
10 9 adantr ${⊢}\left({A}\in ℂ\wedge {B}\subseteq ℂ\right)\to \left(\left({x}\in ℂ\wedge {x}-{A}\in {B}\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}={y}+{A}\right)$
11 ssel2 ${⊢}\left({B}\subseteq ℂ\wedge {y}\in {B}\right)\to {y}\in ℂ$
12 addcl ${⊢}\left({y}\in ℂ\wedge {A}\in ℂ\right)\to {y}+{A}\in ℂ$
13 11 12 sylan ${⊢}\left(\left({B}\subseteq ℂ\wedge {y}\in {B}\right)\wedge {A}\in ℂ\right)\to {y}+{A}\in ℂ$
14 pncan ${⊢}\left({y}\in ℂ\wedge {A}\in ℂ\right)\to {y}+{A}-{A}={y}$
15 11 14 sylan ${⊢}\left(\left({B}\subseteq ℂ\wedge {y}\in {B}\right)\wedge {A}\in ℂ\right)\to {y}+{A}-{A}={y}$
16 simplr ${⊢}\left(\left({B}\subseteq ℂ\wedge {y}\in {B}\right)\wedge {A}\in ℂ\right)\to {y}\in {B}$
17 15 16 eqeltrd ${⊢}\left(\left({B}\subseteq ℂ\wedge {y}\in {B}\right)\wedge {A}\in ℂ\right)\to {y}+{A}-{A}\in {B}$
18 13 17 jca ${⊢}\left(\left({B}\subseteq ℂ\wedge {y}\in {B}\right)\wedge {A}\in ℂ\right)\to \left({y}+{A}\in ℂ\wedge {y}+{A}-{A}\in {B}\right)$
19 18 ancoms ${⊢}\left({A}\in ℂ\wedge \left({B}\subseteq ℂ\wedge {y}\in {B}\right)\right)\to \left({y}+{A}\in ℂ\wedge {y}+{A}-{A}\in {B}\right)$
20 19 anassrs ${⊢}\left(\left({A}\in ℂ\wedge {B}\subseteq ℂ\right)\wedge {y}\in {B}\right)\to \left({y}+{A}\in ℂ\wedge {y}+{A}-{A}\in {B}\right)$
21 eleq1 ${⊢}{x}={y}+{A}\to \left({x}\in ℂ↔{y}+{A}\in ℂ\right)$
22 oveq1 ${⊢}{x}={y}+{A}\to {x}-{A}={y}+{A}-{A}$
23 22 eleq1d ${⊢}{x}={y}+{A}\to \left({x}-{A}\in {B}↔{y}+{A}-{A}\in {B}\right)$
24 21 23 anbi12d ${⊢}{x}={y}+{A}\to \left(\left({x}\in ℂ\wedge {x}-{A}\in {B}\right)↔\left({y}+{A}\in ℂ\wedge {y}+{A}-{A}\in {B}\right)\right)$
25 20 24 syl5ibrcom ${⊢}\left(\left({A}\in ℂ\wedge {B}\subseteq ℂ\right)\wedge {y}\in {B}\right)\to \left({x}={y}+{A}\to \left({x}\in ℂ\wedge {x}-{A}\in {B}\right)\right)$
26 25 rexlimdva ${⊢}\left({A}\in ℂ\wedge {B}\subseteq ℂ\right)\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}={y}+{A}\to \left({x}\in ℂ\wedge {x}-{A}\in {B}\right)\right)$
27 10 26 impbid ${⊢}\left({A}\in ℂ\wedge {B}\subseteq ℂ\right)\to \left(\left({x}\in ℂ\wedge {x}-{A}\in {B}\right)↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}={y}+{A}\right)$
28 27 abbidv ${⊢}\left({A}\in ℂ\wedge {B}\subseteq ℂ\right)\to \left\{{x}|\left({x}\in ℂ\wedge {x}-{A}\in {B}\right)\right\}=\left\{{x}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}={y}+{A}\right\}$
29 1 28 syl5eq ${⊢}\left({A}\in ℂ\wedge {B}\subseteq ℂ\right)\to \left\{{x}\in ℂ|{x}-{A}\in {B}\right\}=\left\{{x}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}={y}+{A}\right\}$