Theorem snres0

Description: Condition for restriction of a singleton to be empty. (Contributed by Scott Fenton, 9-Aug-2024)

	Ref	Expression
Hypothesis	snres0.1	$$⊢B\in \mathrm{V}$$
Assertion	snres0	$$⊢{\left\{⟨A,B⟩\right\}\upharpoonright }_C=\varnothing \leftrightarrow \neg A\in C$$

Proof

Step	Hyp	Ref	Expression
1		snres0.1	$$⊢B\in \mathrm{V}$$
2		relres	$$⊢\mathrm{Rel}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_C\right)$$
3		reldm0	$$⊢\mathrm{Rel}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_C\right)\to \left({\left\{⟨A,B⟩\right\}\upharpoonright }_C=\varnothing \leftrightarrow \mathrm{dom}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_C\right)=\varnothing \right)$$
4	2 3	ax-mp	$$⊢{\left\{⟨A,B⟩\right\}\upharpoonright }_C=\varnothing \leftrightarrow \mathrm{dom}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_C\right)=\varnothing$$
5		dmres	$$⊢\mathrm{dom}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_C\right)=C\cap \mathrm{dom}\left\{⟨A,B⟩\right\}$$
6	1	dmsnop	$$⊢\mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}$$
7	6	ineq2i	$$⊢C\cap \mathrm{dom}\left\{⟨A,B⟩\right\}=C\cap \left\{A\right\}$$
8	5 7	eqtri	$$⊢\mathrm{dom}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_C\right)=C\cap \left\{A\right\}$$
9	8	eqeq1i	$$⊢\mathrm{dom}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_C\right)=\varnothing \leftrightarrow C\cap \left\{A\right\}=\varnothing$$
10		disjsn	$$⊢C\cap \left\{A\right\}=\varnothing \leftrightarrow \neg A\in C$$
11	4 9 10	3bitri	$$⊢{\left\{⟨A,B⟩\right\}\upharpoonright }_C=\varnothing \leftrightarrow \neg A\in C$$