Theorem nfdfat

Description: Bound-variable hypothesis builder for "defined at". To prove a deduction version of this theorem is not easily possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of "defined at" is based on are not available (e.g., for Fun/Rel, dom, C_ , etc.). (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypotheses	nfdfat.1	$$⊢\underset{\_}{Ⅎ}xF$$
	nfdfat.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfdfat	$$⊢ℲxF\mathrm{defAt}A$$

Proof

Step	Hyp	Ref	Expression
1		nfdfat.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		nfdfat.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-dfat	$$⊢F\mathrm{defAt}A\leftrightarrow \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
4	1	nfdm	$$⊢\underset{\_}{Ⅎ}x\mathrm{dom}F$$
5	2 4	nfel	$$⊢ℲxA\in \mathrm{dom}F$$
6	2	nfsn	$$⊢\underset{\_}{Ⅎ}x\left\{A\right\}$$
7	1 6	nfres	$$⊢\underset{\_}{Ⅎ}x\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
8	7	nffun	$$⊢Ⅎx\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
9	5 8	nfan	$$⊢Ⅎx\left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
10	3 9	nfxfr	$$⊢ℲxF\mathrm{defAt}A$$