Metamath Proof Explorer

Theorem fvmptt

Description: Closed theorem form of fvmpt . (Contributed by Scott Fenton, 21-Feb-2013) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Assertion fvmptt 
|- ( ( A. x ( x = A -> B = C ) /\ F = ( x e. D |-> B ) /\ ( A e. D /\ C e. V ) ) -> ( F ` A ) = C )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A. x ( x = A -> B = C ) /\ F = ( x e. D |-> B ) /\ ( A e. D /\ C e. V ) ) -> F = ( x e. D |-> B ) )
2 1 fveq1d 
 |-  ( ( A. x ( x = A -> B = C ) /\ F = ( x e. D |-> B ) /\ ( A e. D /\ C e. V ) ) -> ( F ` A ) = ( ( x e. D |-> B ) ` A ) )
3 risset 
 |-  ( A e. D <-> E. x e. D x = A )
4 elex 
 |-  ( C e. V -> C e. _V )
5 nfa1 
 |-  F/ x A. x ( x = A -> B = C )
6 nfv 
 |-  F/ x C e. _V
7 nffvmpt1 
 |-  F/_ x ( ( x e. D |-> B ) ` A )
8 7 nfeq1 
 |-  F/ x ( ( x e. D |-> B ) ` A ) = C
9 6 8 nfim 
 |-  F/ x ( C e. _V -> ( ( x e. D |-> B ) ` A ) = C )
10 simprl 
 |-  ( ( ( x = A /\ B = C ) /\ ( x e. D /\ C e. _V ) ) -> x e. D )
11 simplr 
 |-  ( ( ( x = A /\ B = C ) /\ ( x e. D /\ C e. _V ) ) -> B = C )
12 simprr 
 |-  ( ( ( x = A /\ B = C ) /\ ( x e. D /\ C e. _V ) ) -> C e. _V )
13 11 12 eqeltrd 
 |-  ( ( ( x = A /\ B = C ) /\ ( x e. D /\ C e. _V ) ) -> B e. _V )
14 eqid 
 |-  ( x e. D |-> B ) = ( x e. D |-> B )
15 14 fvmpt2 
 |-  ( ( x e. D /\ B e. _V ) -> ( ( x e. D |-> B ) ` x ) = B )
16 10 13 15 syl2anc 
 |-  ( ( ( x = A /\ B = C ) /\ ( x e. D /\ C e. _V ) ) -> ( ( x e. D |-> B ) ` x ) = B )
17 simpll 
 |-  ( ( ( x = A /\ B = C ) /\ ( x e. D /\ C e. _V ) ) -> x = A )
18 17 fveq2d 
 |-  ( ( ( x = A /\ B = C ) /\ ( x e. D /\ C e. _V ) ) -> ( ( x e. D |-> B ) ` x ) = ( ( x e. D |-> B ) ` A ) )
19 16 18 11 3eqtr3d 
 |-  ( ( ( x = A /\ B = C ) /\ ( x e. D /\ C e. _V ) ) -> ( ( x e. D |-> B ) ` A ) = C )
20 19 exp43 
 |-  ( x = A -> ( B = C -> ( x e. D -> ( C e. _V -> ( ( x e. D |-> B ) ` A ) = C ) ) ) )
21 20 a2i 
 |-  ( ( x = A -> B = C ) -> ( x = A -> ( x e. D -> ( C e. _V -> ( ( x e. D |-> B ) ` A ) = C ) ) ) )
22 21 com23 
 |-  ( ( x = A -> B = C ) -> ( x e. D -> ( x = A -> ( C e. _V -> ( ( x e. D |-> B ) ` A ) = C ) ) ) )
23 22 sps 
 |-  ( A. x ( x = A -> B = C ) -> ( x e. D -> ( x = A -> ( C e. _V -> ( ( x e. D |-> B ) ` A ) = C ) ) ) )
24 5 9 23 rexlimd 
 |-  ( A. x ( x = A -> B = C ) -> ( E. x e. D x = A -> ( C e. _V -> ( ( x e. D |-> B ) ` A ) = C ) ) )
25 4 24 syl7 
 |-  ( A. x ( x = A -> B = C ) -> ( E. x e. D x = A -> ( C e. V -> ( ( x e. D |-> B ) ` A ) = C ) ) )
26 3 25 syl5bi 
 |-  ( A. x ( x = A -> B = C ) -> ( A e. D -> ( C e. V -> ( ( x e. D |-> B ) ` A ) = C ) ) )
27 26 imp32 
 |-  ( ( A. x ( x = A -> B = C ) /\ ( A e. D /\ C e. V ) ) -> ( ( x e. D |-> B ) ` A ) = C )
28 27 3adant2 
 |-  ( ( A. x ( x = A -> B = C ) /\ F = ( x e. D |-> B ) /\ ( A e. D /\ C e. V ) ) -> ( ( x e. D |-> B ) ` A ) = C )
29 2 28 eqtrd 
 |-  ( ( A. x ( x = A -> B = C ) /\ F = ( x e. D |-> B ) /\ ( A e. D /\ C e. V ) ) -> ( F ` A ) = C )