Theorem resinsn

Description: Restriction to the intersection with a singleton. (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Assertion	resinsn	$$⊢{F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}=\varnothing \leftrightarrow \neg B\in \left(\mathrm{dom}F\cap A\right)$$

Proof

Step	Hyp	Ref	Expression
1		relres	$$⊢\mathrm{Rel}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)$$
2		reldm0	$$⊢\mathrm{Rel}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)\to \left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}=\varnothing \leftrightarrow \mathrm{dom}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)=\varnothing \right)$$
3	1 2	ax-mp	$$⊢{F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}=\varnothing \leftrightarrow \mathrm{dom}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)=\varnothing$$
4		incom	$$⊢\left(A\cap \left\{B\right\}\right)\cap \mathrm{dom}F=\mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)$$
5		dmres	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)=\left(A\cap \left\{B\right\}\right)\cap \mathrm{dom}F$$
6		inass	$$⊢\left(\mathrm{dom}F\cap A\right)\cap \left\{B\right\}=\mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)$$
7	4 5 6	3eqtr4i	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)=\left(\mathrm{dom}F\cap A\right)\cap \left\{B\right\}$$
8	7	eqeq1i	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)=\varnothing \leftrightarrow \left(\mathrm{dom}F\cap A\right)\cap \left\{B\right\}=\varnothing$$
9		disjsn	$$⊢\left(\mathrm{dom}F\cap A\right)\cap \left\{B\right\}=\varnothing \leftrightarrow \neg B\in \left(\mathrm{dom}F\cap A\right)$$
10	3 8 9	3bitri	$$⊢{F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}=\varnothing \leftrightarrow \neg B\in \left(\mathrm{dom}F\cap A\right)$$