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	$$⊢\underset{\_}{Ⅎ}xA$$
	fvmptf.2	$$⊢\underset{\_}{Ⅎ}xC$$
	fvmptf.3	$$⊢x=A\to B=C$$
	fvmptf.4	$$⊢F=\left(x\in D⟼B\right)$$
Assertion	fvmptf	$$⊢\left(A\in D\wedge C\in V\right)\to F\left(A\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		fvmptf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		fvmptf.2	$$⊢\underset{\_}{Ⅎ}xC$$
3		fvmptf.3	$$⊢x=A\to B=C$$
4		fvmptf.4	$$⊢F=\left(x\in D⟼B\right)$$
5	2	nfel1	$$⊢ℲxC\in \mathrm{V}$$
6		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in D⟼B\right)$$
7	4 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}xF$$
8	7 1	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(A\right)$$
9	8 2	nfeq	$$⊢ℲxF\left(A\right)=C$$
10	5 9	nfim	$$⊢Ⅎx\left(C\in \mathrm{V}\to F\left(A\right)=C\right)$$
11	3	eleq1d	$$⊢x=A\to \left(B\in \mathrm{V}\leftrightarrow C\in \mathrm{V}\right)$$
12		fveq2	$$⊢x=A\to F\left(x\right)=F\left(A\right)$$
13	12 3	eqeq12d	$$⊢x=A\to \left(F\left(x\right)=B\leftrightarrow F\left(A\right)=C\right)$$
14	11 13	imbi12d	$$⊢x=A\to \left(\left(B\in \mathrm{V}\to F\left(x\right)=B\right)\leftrightarrow \left(C\in \mathrm{V}\to F\left(A\right)=C\right)\right)$$
15	4	fvmpt2	$$⊢\left(x\in D\wedge B\in \mathrm{V}\right)\to F\left(x\right)=B$$
16	15	ex	$$⊢x\in D\to \left(B\in \mathrm{V}\to F\left(x\right)=B\right)$$
17	1 10 14 16	vtoclgaf	$$⊢A\in D\to \left(C\in \mathrm{V}\to F\left(A\right)=C\right)$$
18		elex	$$⊢C\in V\to C\in \mathrm{V}$$
19	17 18	impel	$$⊢\left(A\in D\wedge C\in V\right)\to F\left(A\right)=C$$