This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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		ffvelcdm	\|- ( ( 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	biimtrid	\|- ( 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 )