Theorem fexafv2ex

Description: The alternate function value is always a set if the function (resp. the domain of the function) is a set. (Contributed by AV, 3-Sep-2022)

	Ref	Expression
Assertion	fexafv2ex	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 '''' 𝐴 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		rnexg	⊢ ( 𝐹 ∈ 𝑉 → ran 𝐹 ∈ V )
2		afv2ex	⊢ ( ran 𝐹 ∈ V → ( 𝐹 '''' 𝐴 ) ∈ V )
3	1 2	syl	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 '''' 𝐴 ) ∈ V )