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	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 '''' 𝐶 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
2		ssexg	⊢ ( ( ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → ran 𝐹 ∈ V )
3	2	ex	⊢ ( ran 𝐹 ⊆ 𝐵 → ( 𝐵 ∈ 𝑉 → ran 𝐹 ∈ V ) )
4	1 3	simplbiim	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐵 ∈ 𝑉 → ran 𝐹 ∈ V ) )
5	4	imp	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → ran 𝐹 ∈ V )
6		afv2ex	⊢ ( ran 𝐹 ∈ V → ( 𝐹 '''' 𝐶 ) ∈ V )
7	5 6	syl	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 '''' 𝐶 ) ∈ V )