Metamath Proof Explorer


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 W k A F k V F : A W F : A V

Proof

Step Hyp Ref Expression
1 simpr V W k A F k V k A F k V
2 ffn F : A W F Fn A
3 1 2 anim12ci V W k A F k V F : A W F Fn A k A F k V
4 ffnfv F : A V F Fn A k A F k V
5 3 4 sylibr V W k A F k V F : A W F : A V
6 simpl V W k A F k V V W
7 6 anim1ci V W k A F k V F : A V F : A V V W
8 fss F : A V V W F : A W
9 7 8 syl V W k A F k V F : A V F : A W
10 5 9 impbida V W k A F k V F : A W F : A V