Theorem fin1a2lem3

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 7-Nov-2014)

	Ref	Expression
Hypothesis	fin1a2lem.b	⊢ 𝐸 = ( 𝑥 ∈ ω ↦ ( 2o ·o 𝑥 ) )
Assertion	fin1a2lem3	⊢ ( 𝐴 ∈ ω → ( 𝐸 ‘ 𝐴 ) = ( 2o ·o 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.b	⊢ 𝐸 = ( 𝑥 ∈ ω ↦ ( 2o ·o 𝑥 ) )
2		oveq2	⊢ ( 𝑎 = 𝐴 → ( 2o ·o 𝑎 ) = ( 2o ·o 𝐴 ) )
3		oveq2	⊢ ( 𝑥 = 𝑎 → ( 2o ·o 𝑥 ) = ( 2o ·o 𝑎 ) )
4	3	cbvmptv	⊢ ( 𝑥 ∈ ω ↦ ( 2o ·o 𝑥 ) ) = ( 𝑎 ∈ ω ↦ ( 2o ·o 𝑎 ) )
5	1 4	eqtri	⊢ 𝐸 = ( 𝑎 ∈ ω ↦ ( 2o ·o 𝑎 ) )
6		ovex	⊢ ( 2o ·o 𝐴 ) ∈ V
7	2 5 6	fvmpt	⊢ ( 𝐴 ∈ ω → ( 𝐸 ‘ 𝐴 ) = ( 2o ·o 𝐴 ) )