This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvmpt2d

Description: Deduction version of fvmpt2 . (Contributed by Thierry Arnoux, 8-Dec-2016)

Ref Expression
Hypotheses fvmpt2d.1 
|- ( ph -> F = ( x e. A |-> B ) )
fvmpt2d.4 
|- ( ( ph /\ x e. A ) -> B e. V )
Assertion fvmpt2d 
|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )

Proof

Step Hyp Ref Expression
1 fvmpt2d.1 
 |-  ( ph -> F = ( x e. A |-> B ) )
2 fvmpt2d.4 
 |-  ( ( ph /\ x e. A ) -> B e. V )
3 1 fveq1d 
 |-  ( ph -> ( F ` x ) = ( ( x e. A |-> B ) ` x ) )
4 3 adantr 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = ( ( x e. A |-> B ) ` x ) )
5 id 
 |-  ( x e. A -> x e. A )
6 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
7 6 fvmpt2 
 |-  ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B )
8 5 2 7 syl2an2 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
9 4 8 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = B )