Definition df-dfat 38617

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.)

Assertion

Ref	Expression
df-dfat	|- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )

Detailed syntax breakdown of Definition df-dfat

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cF	. . 3 class F
3	1, 2	wdfat 38614	. 2 wff F defAt A
4	2	cdm 4834	. . . 4 class dom F
5	1, 4	wcel 1887	. . 3 wff A e. dom F
6	1	csn 3968	. . . . 5 class { A }
7	2, 6	cres 4836	. . . 4 class ( F |` { A } )
8	7	wfun 5576	. . 3 wff Fun ( F |` { A } )
9	5, 8	wa 371	. 2 wff ( A e. dom F /\ Fun ( F |` { A } ) )
10	3, 9	wb 188	1 wff ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )

This definition is referenced by:  dfateq12d  38631  nfdfat  38632  dfdfat2  38633  ndmafv  38642  nfunsnafv  38644  afvpcfv0  38648  afvfvn0fveq  38652  afv0nbfvbi  38653  fnbrafvb  38656  afvelrn  38670  afvres  38674  tz6.12-afv  38675  dmfcoafv  38677  afvco2  38678  aovmpt4g  38703