Definition df-dfat 47583

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

Assertion

Ref	Expression
df-dfat	⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))

Detailed syntax breakdown of Definition df-dfat

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cF	. . 3 class 𝐹
3	1, 2	wdfat 47580	. 2 wff 𝐹 defAt 𝐴
4	2	cdm 5625	. . . 4 class dom 𝐹
5	1, 4	wcel 2119	. . 3 wff 𝐴 ∈ dom 𝐹
6	1	csn 4562	. . . . 5 class {𝐴}
7	2, 6	cres 5627	. . . 4 class (𝐹 ↾ {𝐴})
8	7	wfun 6486	. . 3 wff Fun (𝐹 ↾ {𝐴})
9	5, 8	wa 396	. 2 wff (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))
10	3, 9	wb 207	1 wff (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))

This definition is referenced by:  dfateq12d  47590  nfdfat  47591  dfdfat2  47592  fundmdfat  47593  dfatprc  47594  dfatelrn  47595  ndmafv  47604  nfunsnafv  47606  afvpcfv0  47610  afvfvn0fveq  47614  afv0nbfvbi  47615  fnbrafvb  47618  afvelrn  47632  afvres  47636  tz6.12-afv  47637  dmfcoafv  47639  afvco2  47640  aovmpt4g  47665  ndmafv2nrn  47686  funressndmafv2rn  47687  nfunsnafv2  47689  dmafv2rnb  47693  afv2res  47703  tz6.12-afv2  47704  dfatbrafv2b  47709  dfatdmfcoafv2  47718  dfatcolem  47719  dfatco  47720  afv2ndeffv0  47724  afv2fvn0fveq  47728