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 V
Assertion shftdm A dom F shift A = x | x A dom F

Proof

Step Hyp Ref Expression
1 shftfval.1 F V
2 1 shftfval A F shift A = x y | x x A F y
3 2 dmeqd A dom F shift A = dom x y | x x A F y
4 19.42v y x x A F y x y x A F y
5 ovex x A V
6 5 eldm x A dom F y x A F y
7 6 anbi2i x x A dom F x y x A F y
8 4 7 bitr4i y x x A F y x x A dom F
9 8 abbii x | y x x A F y = x | x x A dom F
10 dmopab dom x y | x x A F y = x | y x x A F y
11 df-rab x | x A dom F = x | x x A dom F
12 9 10 11 3eqtr4i dom x y | x x A F y = x | x A dom F
13 3 12 eqtrdi A dom F shift A = x | x A dom F