Metamath Proof Explorer


Theorem ndfatafv2undef

Description: The alternate function value at a class A is undefined if the function, whose range is a set, is not defined at A . (Contributed by AV, 2-Sep-2022)

Ref Expression
Assertion ndfatafv2undef ran F V ¬ F defAt A F '''' A = Undef ran F

Proof

Step Hyp Ref Expression
1 ndfatafv2 ¬ F defAt A F '''' A = 𝒫 ran F
2 undefval ran F V Undef ran F = 𝒫 ran F
3 2 eqcomd ran F V 𝒫 ran F = Undef ran F
4 1 3 sylan9eqr ran F V ¬ F defAt A F '''' A = Undef ran F