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

Definition df-fun 4013
Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 4447, dffun3 4448, dffun4 4449, dffun5 4450, dffun6 4452, dffun7 4462, dffun8 4463, and dffun9 4464.
Assertion
Ref Expression
df-fun

Detailed syntax breakdown of Definition df-fun
StepHypRef Expression
1 cA . . 3
21wfun 3997 . 2
31wrel 3996 . . 3
41ccnv 3990 . . . . 5
51, 4ccom 3995 . . . 4
6 cid 3607 . . . 4
75, 6wss 2634 . . 3
83, 7wa 360 . 2
92, 8wb 174 1
Colors of variables: wff set class
This definition is referenced by:  dffun2 4447  funrel 4454  funss 4455  hbfun 4459  funi 4466  f1ococnv2 4653  dffv2 4732  flimfnei2 16296  cnvcan 17191
Copyright terms: Public domain