**Description:** A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016)

Ref | Expression | ||
---|---|---|---|

Hypotheses | ffvelrnd.1 | $${\u22a2}{\phi}\to {F}:{A}\u27f6{B}$$ | |

ffvelrnd.2 | $${\u22a2}{\phi}\to {C}\in {A}$$ | ||

Assertion | ffvelrnd | $${\u22a2}{\phi}\to {F}\left({C}\right)\in {B}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | ffvelrnd.1 | $${\u22a2}{\phi}\to {F}:{A}\u27f6{B}$$ | |

2 | ffvelrnd.2 | $${\u22a2}{\phi}\to {C}\in {A}$$ | |

3 | 1 | ffvelrnda | $${\u22a2}\left({\phi}\wedge {C}\in {A}\right)\to {F}\left({C}\right)\in {B}$$ |

4 | 2 3 | mpdan | $${\u22a2}{\phi}\to {F}\left({C}\right)\in {B}$$ |