Theorem shftidt2

Description: Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013)

	Ref	Expression
Hypothesis	shftfval.1	⊢ 𝐹 ∈ V
Assertion	shftidt2	⊢ ( 𝐹 shift 0 ) = ( 𝐹 ↾ ℂ )

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	⊢ 𝐹 ∈ V
2		subid1	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 − 0 ) = 𝑥 )
3	2	breq1d	⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 − 0 ) 𝐹 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
4	3	pm5.32i	⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 0 ) 𝐹 𝑦 ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 𝐹 𝑦 ) )
5	4	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 0 ) 𝐹 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑥 𝐹 𝑦 ) }
6		0cn	⊢ 0 ∈ ℂ
7	1	shftfval	⊢ ( 0 ∈ ℂ → ( 𝐹 shift 0 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 0 ) 𝐹 𝑦 ) } )
8	6 7	ax-mp	⊢ ( 𝐹 shift 0 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 0 ) 𝐹 𝑦 ) }
9		dfres2	⊢ ( 𝐹 ↾ ℂ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑥 𝐹 𝑦 ) }
10	5 8 9	3eqtr4i	⊢ ( 𝐹 shift 0 ) = ( 𝐹 ↾ ℂ )