Theorem fvmptmap

Description: Special case of fvmpt for operator theorems. (Contributed by NM, 27-Nov-2007)

	Ref	Expression
Hypotheses	fvmptmap.1	$$⊢C\in \mathrm{V}$$
	fvmptmap.2	$$⊢D\in \mathrm{V}$$
	fvmptmap.3	$$⊢R\in \mathrm{V}$$
	fvmptmap.4	$$⊢x=A\to B=C$$
	fvmptmap.5	$$⊢F=\left(x\in \left(R^D\right)⟼B\right)$$
Assertion	fvmptmap	$$⊢A:D⟶R\to F\left(A\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		fvmptmap.1	$$⊢C\in \mathrm{V}$$
2		fvmptmap.2	$$⊢D\in \mathrm{V}$$
3		fvmptmap.3	$$⊢R\in \mathrm{V}$$
4		fvmptmap.4	$$⊢x=A\to B=C$$
5		fvmptmap.5	$$⊢F=\left(x\in \left(R^D\right)⟼B\right)$$
6	3 2	elmap	$$⊢A\in \left(R^D\right)\leftrightarrow A:D⟶R$$
7	4 5 1	fvmpt	$$⊢A\in \left(R^D\right)\to F\left(A\right)=C$$
8	6 7	sylbir	$$⊢A:D⟶R\to F\left(A\right)=C$$