Theorem nfunsnaov

Description: If the restriction of a class to a singleton is not a function, its operation value is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	nfunsnaov	⊢ ( ¬ Fun ( 𝐹 ↾ { ⟨ 𝐴 , 𝐵 ⟩ } ) → (( 𝐴 𝐹 𝐵 )) = V )

Proof

Step	Hyp	Ref	Expression
1		df-aov	⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )
2		nfunsnafv	⊢ ( ¬ Fun ( 𝐹 ↾ { ⟨ 𝐴 , 𝐵 ⟩ } ) → ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = V )
3	1 2	eqtrid	⊢ ( ¬ Fun ( 𝐹 ↾ { ⟨ 𝐴 , 𝐵 ⟩ } ) → (( 𝐴 𝐹 𝐵 )) = V )