Definition df-dfat

Description: Definition of the predicate that determines if some class F is defined as function for an argument A or, in other words, if the function value for some class F for an argument A is defined. We say that F is defined at A if a F is a function restricted to the member A of its domain. (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	df-dfat	$$⊢F\mathrm{defAt}A\leftrightarrow \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1		cA	$$classA$$
2	1 0	wdfat	$$wffF\mathrm{defAt}A$$
3	0	cdm	$$class\mathrm{dom}F$$
4	1 3	wcel	$$wffA\in \mathrm{dom}F$$
5	1	csn	$$class\left\{A\right\}$$
6	0 5	cres	$$class\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
7	6	wfun	$$wff\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
8	4 7	wa	$$wff\left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
9	2 8	wb	$$wff\left(F\mathrm{defAt}A\leftrightarrow \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)\right)$$