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	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1		cA	⊢ 𝐴
2	1 0	wdfat	⊢ 𝐹 defAt 𝐴
3	0	cdm	⊢ dom 𝐹
4	1 3	wcel	⊢ 𝐴 ∈ dom 𝐹
5	1	csn	⊢ { 𝐴 }
6	0 5	cres	⊢ ( 𝐹 ↾ { 𝐴 } )
7	6	wfun	⊢ Fun ( 𝐹 ↾ { 𝐴 } )
8	4 7	wa	⊢ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) )
9	2 8	wb	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )