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 defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	|- F
1		cA	|- A
2	1 0	wdfat	|- F defAt A
3	0	cdm	|- dom F
4	1 3	wcel	|- A e. dom F
5	1	csn	|- { A }
6	0 5	cres	|- ( F |` { A } )
7	6	wfun	|- Fun ( F |` { A } )
8	4 7	wa	|- ( A e. dom F /\ Fun ( F |` { A } ) )
9	2 8	wb	|- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )