Theorem ndmafv

Description: The value of a class outside its domain is the universe, compare with ndmfv . (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	ndmafv	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ''' 𝐴 ) = V )

Proof

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