Theorem afv2ex

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

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

Proof

Step	Hyp	Ref	Expression
1		df-afv2	⊢ ( 𝐹 '''' 𝐴 ) = if ( 𝐹 defAt 𝐴 , ( ℩ 𝑥 𝐴 𝐹 𝑥 ) , 𝒫 ∪ ran 𝐹 )
2		iotaex	⊢ ( ℩ 𝑥 𝐴 𝐹 𝑥 ) ∈ V
3	2	a1i	⊢ ( ran 𝐹 ∈ 𝑉 → ( ℩ 𝑥 𝐴 𝐹 𝑥 ) ∈ V )
4		uniexg	⊢ ( ran 𝐹 ∈ 𝑉 → ∪ ran 𝐹 ∈ V )
5	4	pwexd	⊢ ( ran 𝐹 ∈ 𝑉 → 𝒫 ∪ ran 𝐹 ∈ V )
6	3 5	ifcld	⊢ ( ran 𝐹 ∈ 𝑉 → if ( 𝐹 defAt 𝐴 , ( ℩ 𝑥 𝐴 𝐹 𝑥 ) , 𝒫 ∪ ran 𝐹 ) ∈ V )
7	1 6	eqeltrid	⊢ ( ran 𝐹 ∈ 𝑉 → ( 𝐹 '''' 𝐴 ) ∈ V )