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 e. V /\ -. F defAt A ) -> ( F '''' A ) = ( Undef ` ran F ) )

Proof

Step Hyp Ref Expression
1 ndfatafv2
 |-  ( -. F defAt A -> ( F '''' A ) = ~P U. ran F )
2 undefval
 |-  ( ran F e. V -> ( Undef ` ran F ) = ~P U. ran F )
3 2 eqcomd
 |-  ( ran F e. V -> ~P U. ran F = ( Undef ` ran F ) )
4 1 3 sylan9eqr
 |-  ( ( ran F e. V /\ -. F defAt A ) -> ( F '''' A ) = ( Undef ` ran F ) )