Theorem fvmptndm

Description: Value of a function given by the maps-to notation, outside of its domain. (Contributed by AV, 31-Dec-2020)

	Ref	Expression
Hypothesis	fvmptndm.1	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	fvmptndm	$$⊢\neg X\in A\to F\left(X\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		fvmptndm.1	$$⊢F=\left(x\in A⟼B\right)$$
2		df-mpt	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
3	1 2	eqtri	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
4	3	fvopab4ndm	$$⊢\neg X\in A\to F\left(X\right)=\varnothing$$