Theorem nfunsnafv

Description: If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn . (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	nfunsnafv	⊢ ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹 ''' 𝐴 ) = V )

Proof

Step	Hyp	Ref	Expression
1		df-dfat	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
2	1	simprbi	⊢ ( 𝐹 defAt 𝐴 → Fun ( 𝐹 ↾ { 𝐴 } ) )
3		afvnfundmuv	⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 ''' 𝐴 ) = V )
4	2 3	nsyl5	⊢ ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹 ''' 𝐴 ) = V )