Metamath Proof Explorer

Theorem fcdmssb

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 fcdmssb ⊢V⊆W∧∀k∈AF⁡k∈V→F:A⟶W↔F:A⟶V

Proof

Step Hyp Ref Expression
1 simpr ⊢V⊆W∧∀k∈AF⁡k∈V→∀k∈AF⁡k∈V
2 ffn ⊢F:A⟶W→FFnA
3 1 2 anim12ci ⊢V⊆W∧∀k∈AF⁡k∈V∧F:A⟶W→FFnA∧∀k∈AF⁡k∈V
4 ffnfv ⊢F:A⟶V↔FFnA∧∀k∈AF⁡k∈V
5 3 4 sylibr ⊢V⊆W∧∀k∈AF⁡k∈V∧F:A⟶W→F:A⟶V
6 simpl ⊢V⊆W∧∀k∈AF⁡k∈V→V⊆W
7 6 anim1ci ⊢V⊆W∧∀k∈AF⁡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∈AF⁡k∈V∧F:A⟶V→F:A⟶W
10 5 9 impbida ⊢V⊆W∧∀k∈AF⁡k∈V→F:A⟶W↔F:A⟶V