Metamath Proof Explorer

Theorem frnvafv2v

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 frnvafv2v ⊢ F : A ⟶ B ∧ B ∈ V → F '''' C ∈ V

Proof

Step Hyp Ref Expression
1 df-f ⊢ F : A ⟶ B ↔ F Fn A ∧ 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