Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 7-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fin1a2lem.b | ⊢ 𝐸 = ( 𝑥 ∈ ω ↦ ( 2o ·o 𝑥 ) ) | |
Assertion | fin1a2lem3 | ⊢ ( 𝐴 ∈ ω → ( 𝐸 ‘ 𝐴 ) = ( 2o ·o 𝐴 ) ) |
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 𝐴 ) ) |