Metamath Proof Explorer

Theorem fcdmvafv2v

Description: If the codomain of a function is a set, the alternate function value is always also a set. (Contributed by AV, 4-Sep-2022)

Ref Expression
Assertion fcdmvafv2v ⊢F:A⟶B∧B∈V→F''''C∈V

Proof

Step Hyp Ref Expression
1 df-f ⊢F:A⟶B↔FFnA∧ran⁡F⊆B
2 ssexg ⊢ran⁡F⊆B∧B∈V→ran⁡F∈V
3 2 ex ⊢ran⁡F⊆B→B∈V→ran⁡F∈V
4 1 3 simplbiim ⊢F:A⟶B→B∈V→ran⁡F∈V
5 4 imp ⊢F:A⟶B∧B∈V→ran⁡F∈V
6 afv2ex ⊢ran⁡F∈V→F''''C∈V
7 5 6 syl ⊢F:A⟶B∧B∈V→F''''C∈V