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

Definition df-fun 4043
Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 4502, dffun3 4503, dffun4 4504, dffun5 4505, dffun6 4507, dffun7 4517, dffun8 4518, and dffun9 4519.
Assertion
Ref Expression
df-fun

Detailed syntax breakdown of Definition df-fun
StepHypRef Expression
1 cA . . 3
21wfun 4027 . 2
31wrel 4026 . . 3
41ccnv 4020 . . . . 5
51, 4ccom 4025 . . . 4
6 cid 3633 . . . 4
75, 6wss 2636 . . 3
83, 7wa 357 . 2
92, 8wb 174 1
Colors of variables: wff set class
This definition is referenced by:  dffun2 4502  funrel 4509  funss 4510  hbfun 4514  funi 4521  f1ococnv2 4714  funcocnv2 4718  dffv2 4797  flfnei2 18301
Copyright terms: Public domain