New Foundations Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-fun		Unicode version

---

Definition df-fun 4789

Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 5119, dffun3 5120, dffun4 5121, dffun5 5122, dffun6 5124, dffun7 5133, dffun8 5134, and dffun9 5135. (Contributed by SF, 5-Jan-2015.) (Revised by Scott Fenton, 14-Apr-2021.)

Assertion

Ref	Expression
df-fun

---

Detailed syntax breakdown of Definition df-fun

Step	Hyp	Ref	Expression
1		cA	. . 3
2	1	wfun 4775	. 2
3	1	ccnv 4771	. . . 4
4	1, 3	ccom 4721	. . 3
5		cid 4763	. . 3
6	4, 5	wss 3257	. 2
7	2, 6	wb 176	1

Colors of variables: wff setvar class

This definition is referenced by:  dffun2  5119  funss  5126  nffun  5130  funi  5137  fun0  5154  f1ococnv2  5309

Copyright terms: Public domain

W3C validator