Theorem fvmptf

Description: Value of a function given by an ordered-pair class abstraction. This version of fvmptg uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005) (Revised by Mario Carneiro, 15-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		fvmptf.1	|- F/_ x A
2		fvmptf.2	|- F/_ x C
3		fvmptf.3	|- ( x = A -> B = C )
4		fvmptf.4	|- F = ( x e. D |-> B )
5	2	nfel1	|- F/ x C e. _V
6		nfmpt1	|- F/_ x ( x e. D |-> B )
7	4 6	nfcxfr	|- F/_ x F
8	7 1	nffv	|- F/_ x ( F ` A )
9	8 2	nfeq	|- F/ x ( F ` A ) = C
10	5 9	nfim	|- F/ x ( C e. _V -> ( F ` A ) = C )
11	3	eleq1d	|- ( x = A -> ( B e. _V <-> C e. _V ) )
12		fveq2	|- ( x = A -> ( F ` x ) = ( F ` A ) )
13	12 3	eqeq12d	|- ( x = A -> ( ( F ` x ) = B <-> ( F ` A ) = C ) )
14	11 13	imbi12d	|- ( x = A -> ( ( B e. _V -> ( F ` x ) = B ) <-> ( C e. _V -> ( F ` A ) = C ) ) )
15	4	fvmpt2	|- ( ( x e. D /\ B e. _V ) -> ( F ` x ) = B )
16	15	ex	|- ( x e. D -> ( B e. _V -> ( F ` x ) = B ) )
17	1 10 14 16	vtoclgaf	|- ( A e. D -> ( C e. _V -> ( F ` A ) = C ) )
18		elex	|- ( C e. V -> C e. _V )
19	17 18	impel	|- ( ( A e. D /\ C e. V ) -> ( F ` A ) = C )