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 = { f | f : A --> B }
	fsetfocdm.s	|- S = ( g e. F |-> ( g ` X ) )
Assertion	fsetfcdm	|- ( X e. A -> S : F --> B )

Proof

Step	Hyp	Ref	Expression
1		fsetfocdm.f	|- F = { f | f : A --> B }
2		fsetfocdm.s	|- S = ( g e. F |-> ( g ` X ) )
3		vex	|- g e. _V
4		feq1	|- ( f = g -> ( f : A --> B <-> g : A --> B ) )
5	3 4 1	elab2	|- ( g e. F <-> g : A --> B )
6		ffvelrn	|- ( ( g : A --> B /\ X e. A ) -> ( g ` X ) e. B )
7	6	expcom	|- ( X e. A -> ( g : A --> B -> ( g ` X ) e. B ) )
8	5 7	syl5bi	|- ( X e. A -> ( g e. F -> ( g ` X ) e. B ) )
9	8	imp	|- ( ( X e. A /\ g e. F ) -> ( g ` X ) e. B )
10	9 2	fmptd	|- ( X e. A -> S : F --> B )