Description: The alternate function value at a class A if the function is not defined at this set A . (Contributed by AV, 2-Sep-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | ndfatafv2 | ⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-afv2 | ⊢ ( 𝐹 '''' 𝐴 ) = if ( 𝐹 defAt 𝐴 , ( ℩ 𝑥 𝐴 𝐹 𝑥 ) , 𝒫 ∪ ran 𝐹 ) | |
2 | iffalse | ⊢ ( ¬ 𝐹 defAt 𝐴 → if ( 𝐹 defAt 𝐴 , ( ℩ 𝑥 𝐴 𝐹 𝑥 ) , 𝒫 ∪ ran 𝐹 ) = 𝒫 ∪ ran 𝐹 ) | |
3 | 1 2 | syl5eq | ⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 ) |