Theorem fnresdisj

Description: A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004)

	Ref	Expression
Assertion	fnresdisj	$$⊢FFnA\to \left(A\cap B=\varnothing \leftrightarrow {F\upharpoonright }_B=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		relres	$$⊢\mathrm{Rel}\left({F\upharpoonright }_B\right)$$
2		reldm0	$$⊢\mathrm{Rel}\left({F\upharpoonright }_B\right)\to \left({F\upharpoonright }_B=\varnothing \leftrightarrow \mathrm{dom}\left({F\upharpoonright }_B\right)=\varnothing \right)$$
3	1 2	ax-mp	$$⊢{F\upharpoonright }_B=\varnothing \leftrightarrow \mathrm{dom}\left({F\upharpoonright }_B\right)=\varnothing$$
4		dmres	$$⊢\mathrm{dom}\left({F\upharpoonright }_B\right)=B\cap \mathrm{dom}F$$
5		incom	$$⊢B\cap \mathrm{dom}F=\mathrm{dom}F\cap B$$
6	4 5	eqtri	$$⊢\mathrm{dom}\left({F\upharpoonright }_B\right)=\mathrm{dom}F\cap B$$
7		fndm	$$⊢FFnA\to \mathrm{dom}F=A$$
8	7	ineq1d	$$⊢FFnA\to \mathrm{dom}F\cap B=A\cap B$$
9	6 8	eqtrid	$$⊢FFnA\to \mathrm{dom}\left({F\upharpoonright }_B\right)=A\cap B$$
10	9	eqeq1d	$$⊢FFnA\to \left(\mathrm{dom}\left({F\upharpoonright }_B\right)=\varnothing \leftrightarrow A\cap B=\varnothing \right)$$
11	3 10	bitr2id	$$⊢FFnA\to \left(A\cap B=\varnothing \leftrightarrow {F\upharpoonright }_B=\varnothing \right)$$