NFE Home 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
StepHypRef Expression
1 cA . . 3
21wfun 4775 . 2
31ccnv 4771 . . . 4
41, 3ccom 4721 . . 3
5 cid 4763 . . 3
64, 5wss 3257 . 2
72, 6wb 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