Metamath Proof Explorer


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