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

Definition df-fun 4029
Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 4485, dffun3 4486, dffun4 4487, dffun5 4488, dffun6 4490, dffun7 4500, dffun8 4501, and dffun9 4502.
Assertion
Ref Expression
df-fun

Detailed syntax breakdown of Definition df-fun
StepHypRef Expression
1 cA . . 3
21wfun 4013 . 2
31wrel 4012 . . 3
41ccnv 4006 . . . . 5
51, 4ccom 4011 . . . 4
6 cid 3619 . . . 4
75, 6wss 2634 . . 3
83, 7wa 357 . 2
92, 8wb 174 1
Colors of variables: wff set class
This definition is referenced by:  dffun2 4485  funrel 4492  funss 4493  hbfun 4497  funi 4504  f1ococnv2 4696  funcocnv2 4700  dffv2 4779  flimfnei2 17553
Copyright terms: Public domain