This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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