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 e. _V
Assertion	shftdm	|- ( A e. CC -> dom ( F shift A ) = { x e. CC | ( x - A ) e. dom F } )

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	|- F e. _V
2	1	shftfval	|- ( A e. CC -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
3	2	dmeqd	|- ( A e. CC -> dom ( F shift A ) = dom { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
4		19.42v	|- ( E. y ( x e. CC /\ ( x - A ) F y ) <-> ( x e. CC /\ E. y ( x - A ) F y ) )
5		ovex	|- ( x - A ) e. _V
6	5	eldm	|- ( ( x - A ) e. dom F <-> E. y ( x - A ) F y )
7	6	anbi2i	|- ( ( x e. CC /\ ( x - A ) e. dom F ) <-> ( x e. CC /\ E. y ( x - A ) F y ) )
8	4 7	bitr4i	|- ( E. y ( x e. CC /\ ( x - A ) F y ) <-> ( x e. CC /\ ( x - A ) e. dom F ) )
9	8	abbii	|- { x | E. y ( x e. CC /\ ( x - A ) F y ) } = { x | ( x e. CC /\ ( x - A ) e. dom F ) }
10		dmopab	|- dom { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } = { x | E. y ( x e. CC /\ ( x - A ) F y ) }
11		df-rab	|- { x e. CC | ( x - A ) e. dom F } = { x | ( x e. CC /\ ( x - A ) e. dom F ) }
12	9 10 11	3eqtr4i	|- dom { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } = { x e. CC | ( x - A ) e. dom F }
13	3 12	eqtrdi	|- ( A e. CC -> dom ( F shift A ) = { x e. CC | ( x - A ) e. dom F } )