Theorem nfvres

Description: The value of a non-member of a restriction is the empty set. (An artifact of our function value definition.) (Contributed by NM, 13-Nov-1995)

	Ref	Expression
Assertion	nfvres	⊢ ( ¬ 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		dmres	⊢ dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
2		inss1	⊢ ( 𝐵 ∩ dom 𝐹 ) ⊆ 𝐵
3	1 2	eqsstri	⊢ dom ( 𝐹 ↾ 𝐵 ) ⊆ 𝐵
4	3	sseli	⊢ ( 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) → 𝐴 ∈ 𝐵 )
5		ndmfv	⊢ ( ¬ 𝐴 ∈ dom ( 𝐹 ↾ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ∅ )
6	4 5	nsyl5	⊢ ( ¬ 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ∅ )