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

Definition df-fun 4056
Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 4524, dffun3 4525, dffun4 4526, dffun5 4527, dffun6 4529, dffun7 4539, dffun8 4540, and dffun9 4541.
Assertion
Ref Expression
df-fun

Detailed syntax breakdown of Definition df-fun
StepHypRef Expression
1 cA . . 3
21wfun 4040 . 2
31wrel 4039 . . 3
41ccnv 4033 . . . . 5
51, 4ccom 4038 . . . 4
6 cid 3645 . . . 4
75, 6wss 2637 . . 3
83, 7wa 357 . 2
92, 8wb 174 1
Colors of variables: wff set class
This definition is referenced by:  dffun2 4524  funrel 4531  funss 4532  hbfun 4536  funi 4543  f1ococnv2 4740  funcocnv2 4744  dffv2 4819  flfnei2 18614
Copyright terms: Public domain