Theorem fin1a2lem3

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

	Ref	Expression
Hypothesis	fin1a2lem.b	|- E = ( x e. _om |-> ( 2o .o x ) )
Assertion	fin1a2lem3	|- ( A e. _om -> ( E ` A ) = ( 2o .o A ) )

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.b	|- E = ( x e. _om |-> ( 2o .o x ) )
2		oveq2	|- ( a = A -> ( 2o .o a ) = ( 2o .o A ) )
3		oveq2	|- ( x = a -> ( 2o .o x ) = ( 2o .o a ) )
4	3	cbvmptv	|- ( x e. _om |-> ( 2o .o x ) ) = ( a e. _om |-> ( 2o .o a ) )
5	1 4	eqtri	|- E = ( a e. _om |-> ( 2o .o a ) )
6		ovex	|- ( 2o .o A ) e. _V
7	2 5 6	fvmpt	|- ( A e. _om -> ( E ` A ) = ( 2o .o A ) )