Theorem fvopab4ndm

Description: Value of a function given by an ordered-pair class abstraction, outside of its domain. (Contributed by NM, 28-Mar-2008)

	Ref	Expression
Hypothesis	fvopab4ndm.1	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
Assertion	fvopab4ndm	$$⊢\neg B\in A\to F\left(B\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		fvopab4ndm.1	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
2	1	dmeqi	$$⊢\mathrm{dom}F=\mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
3		dmopabss	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\subseteq A$$
4	2 3	eqsstri	$$⊢\mathrm{dom}F\subseteq A$$
5	4	sseli	$$⊢B\in \mathrm{dom}F\to B\in A$$
6		ndmfv	$$⊢\neg B\in \mathrm{dom}F\to F\left(B\right)=\varnothing$$
7	5 6	nsyl5	$$⊢\neg B\in A\to F\left(B\right)=\varnothing$$