Theorem frnssb

Description: A function is a function into a subset of its codomain if all of its values are elements of this subset. (Contributed by AV, 7-Feb-2021)

	Ref	Expression
Assertion	frnssb	|- ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) -> ( F : A --> W <-> F : A --> V ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) -> A. k e. A ( F ` k ) e. V )
2		ffn	|- ( F : A --> W -> F Fn A )
3	1 2	anim12ci	|- ( ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) /\ F : A --> W ) -> ( F Fn A /\ A. k e. A ( F ` k ) e. V ) )
4		ffnfv	|- ( F : A --> V <-> ( F Fn A /\ A. k e. A ( F ` k ) e. V ) )
5	3 4	sylibr	|- ( ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) /\ F : A --> W ) -> F : A --> V )
6		simpl	|- ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) -> V C_ W )
7	6	anim1ci	|- ( ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) /\ F : A --> V ) -> ( F : A --> V /\ V C_ W ) )
8		fss	|- ( ( F : A --> V /\ V C_ W ) -> F : A --> W )
9	7 8	syl	|- ( ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) /\ F : A --> V ) -> F : A --> W )
10	5 9	impbida	|- ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) -> ( F : A --> W <-> F : A --> V ) )