HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-fun 4017
Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 4463, dffun3 4464, dffun4 4465, dffun5 4466, dffun6 4468, dffun7 4478, dffun8 4479, and dffun9 4480.
Assertion
Ref Expression
df-fun

Detailed syntax breakdown of Definition df-fun
StepHypRef Expression
1 cA . . 3
21wfun 4001 . 2
31wrel 4000 . . 3
41ccnv 3994 . . . . 5
51, 4ccom 3999 . . . 4
6 cid 3607 . . . 4
75, 6wss 2632 . . 3
83, 7wa 356 . 2
92, 8wb 173 1
Colors of variables: wff set class
This definition is referenced by:  dffun2 4463  funrel 4470  funss 4471  hbfun 4475  funi 4482  f1ococnv2 4670  dffv2 4751  flimfnei2 17212  cnvcan 18107
Copyright terms: Public domain