Theorem fsetfcdm

Description: The class of functions with a given domain and a given codomain is mapped, through evaluation at a point of the domain, into the codomain. (Contributed by AV, 15-Sep-2024)

	Ref	Expression
Hypotheses	fsetfocdm.f	$$⊢F=\left\{f|f:A⟶B\right\}$$
	fsetfocdm.s	$$⊢S=\left(g\in F⟼g\left(X\right)\right)$$
Assertion	fsetfcdm	$$⊢X\in A\to S:F⟶B$$

Proof

Step	Hyp	Ref	Expression
1		fsetfocdm.f	$$⊢F=\left\{f|f:A⟶B\right\}$$
2		fsetfocdm.s	$$⊢S=\left(g\in F⟼g\left(X\right)\right)$$
3		vex	$$⊢g\in \mathrm{V}$$
4		feq1	$$⊢f=g\to \left(f:A⟶B\leftrightarrow g:A⟶B\right)$$
5	3 4 1	elab2	$$⊢g\in F\leftrightarrow g:A⟶B$$
6		ffvelrn	$$⊢\left(g:A⟶B\wedge X\in A\right)\to g\left(X\right)\in B$$
7	6	expcom	$$⊢X\in A\to \left(g:A⟶B\to g\left(X\right)\in B\right)$$
8	5 7	syl5bi	$$⊢X\in A\to \left(g\in F\to g\left(X\right)\in B\right)$$
9	8	imp	$$⊢\left(X\in A\wedge g\in F\right)\to g\left(X\right)\in B$$
10	9 2	fmptd	$$⊢X\in A\to S:F⟶B$$