Theorem cfsetssfset

Description: The class of constant functions is a subclass of the class of functions. (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Hypothesis	cfsetsnfsetfv.f	|- F = { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) }
Assertion	cfsetssfset	|- F C_ { f | f : A --> B }

Proof

Step	Hyp	Ref	Expression
1		cfsetsnfsetfv.f	|- F = { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) }
2		ss2ab	|- ( { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } C_ { f | f : A --> B } <-> A. f ( ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) -> f : A --> B ) )
3		simpl	|- ( ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) -> f : A --> B )
4	2 3	mpgbir	|- { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } C_ { f | f : A --> B }
5	1 4	eqsstri	|- F C_ { f | f : A --> B }