Metamath Proof Explorer

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 ⁡ F ∈ V → F '''' A ∈ V

Proof

Step Hyp Ref Expression
1 df-afv2 ⊢ F '''' A = if F defAt A ι x | A F x 𝒫 ⋃ ran ⁡ F
2 iotaex ⊢ ι x | A F x ∈ V
3 2 a1i ⊢ ran ⁡ F ∈ V → ι x | A F x ∈ V
4 uniexg ⊢ ran ⁡ F ∈ V → ⋃ ran ⁡ F ∈ V
5 4 pwexd ⊢ ran ⁡ F ∈ V → 𝒫 ⋃ ran ⁡ F ∈ V
6 3 5 ifcld ⊢ ran ⁡ F ∈ V → if F defAt A ι x | A F x 𝒫 ⋃ ran ⁡ F ∈ V
7 1 6 eqeltrid ⊢ ran ⁡ F ∈ V → F '''' A ∈ V