Metamath Proof Explorer


Theorem afvnfundmuv

Description: If a set is not in the domain of a class or the class is not a function restricted to the set, then the function value for this set is the universe. (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Assertion afvnfundmuv ¬ F defAt A F ''' A = V

Proof

Step Hyp Ref Expression
1 dfafv2 F ''' A = if F defAt A F A V
2 iffalse ¬ F defAt A if F defAt A F A V = V
3 1 2 syl5eq ¬ F defAt A F ''' A = V