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	⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 ''' 𝐴 ) = V )

Proof

Step	Hyp	Ref	Expression
1		dfafv2	⊢ ( 𝐹 ''' 𝐴 ) = if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V )
2		iffalse	⊢ ( ¬ 𝐹 defAt 𝐴 → if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V ) = V )
3	1 2	syl5eq	⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 ''' 𝐴 ) = V )