Theorem ressnop0

Description: If A is not in C , then the restriction of a singleton of <. A , B >. to C is null. (Contributed by Scott Fenton, 15-Apr-2011)

	Ref	Expression
Assertion	ressnop0	$$⊢\neg A\in C\to {\left\{⟨A,B⟩\right\}\upharpoonright }_C=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		opelxp1	$$⊢⟨A,B⟩\in \left(C\times \mathrm{V}\right)\to A\in C$$
2		df-res	$$⊢{\left\{⟨A,B⟩\right\}\upharpoonright }_C=\left\{⟨A,B⟩\right\}\cap \left(C\times \mathrm{V}\right)$$
3		incom	$$⊢\left\{⟨A,B⟩\right\}\cap \left(C\times \mathrm{V}\right)=\left(C\times \mathrm{V}\right)\cap \left\{⟨A,B⟩\right\}$$
4	2 3	eqtri	$$⊢{\left\{⟨A,B⟩\right\}\upharpoonright }_C=\left(C\times \mathrm{V}\right)\cap \left\{⟨A,B⟩\right\}$$
5		disjsn	$$⊢\left(C\times \mathrm{V}\right)\cap \left\{⟨A,B⟩\right\}=\varnothing \leftrightarrow \neg ⟨A,B⟩\in \left(C\times \mathrm{V}\right)$$
6	5	biimpri	$$⊢\neg ⟨A,B⟩\in \left(C\times \mathrm{V}\right)\to \left(C\times \mathrm{V}\right)\cap \left\{⟨A,B⟩\right\}=\varnothing$$
7	4 6	syl5eq	$$⊢\neg ⟨A,B⟩\in \left(C\times \mathrm{V}\right)\to {\left\{⟨A,B⟩\right\}\upharpoonright }_C=\varnothing$$
8	1 7	nsyl5	$$⊢\neg A\in C\to {\left\{⟨A,B⟩\right\}\upharpoonright }_C=\varnothing$$