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

Metamath Proof Explorer

Theorem fvmptdv2

Description: Alternate deduction version of fvmpt , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017)

Ref Expression
Hypotheses fvmptdv2.1 
|- ( ph -> A e. D )
fvmptdv2.2 
|- ( ( ph /\ x = A ) -> B e. V )
fvmptdv2.3 
|- ( ( ph /\ x = A ) -> B = C )
Assertion fvmptdv2 
|- ( ph -> ( F = ( x e. D |-> B ) -> ( F ` A ) = C ) )

Proof

Step Hyp Ref Expression
1 fvmptdv2.1 
 |-  ( ph -> A e. D )
2 fvmptdv2.2 
 |-  ( ( ph /\ x = A ) -> B e. V )
3 fvmptdv2.3 
 |-  ( ( ph /\ x = A ) -> B = C )
4 eqidd 
 |-  ( ph -> ( x e. D |-> B ) = ( x e. D |-> B ) )
5 1 elexd 
 |-  ( ph -> A e. _V )
6 isset 
 |-  ( A e. _V <-> E. x x = A )
7 5 6 sylib 
 |-  ( ph -> E. x x = A )
8 2 elexd 
 |-  ( ( ph /\ x = A ) -> B e. _V )
9 3 8 eqeltrrd 
 |-  ( ( ph /\ x = A ) -> C e. _V )
10 7 9 exlimddv 
 |-  ( ph -> C e. _V )
11 4 3 1 10 fvmptd 
 |-  ( ph -> ( ( x e. D |-> B ) ` A ) = C )
12 fveq1 
 |-  ( F = ( x e. D |-> B ) -> ( F ` A ) = ( ( x e. D |-> B ) ` A ) )
13 12 eqeq1d 
 |-  ( F = ( x e. D |-> B ) -> ( ( F ` A ) = C <-> ( ( x e. D |-> B ) ` A ) = C ) )
14 11 13 syl5ibrcom 
 |-  ( ph -> ( F = ( x e. D |-> B ) -> ( F ` A ) = C ) )