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