Metamath Proof Explorer


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 𝐴 ) )