ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-f Structured version   Unicode version

Definition df-f 4849
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f  F : -->  F  Fn  ran  F 
C_

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cF . . 3  F
41, 2, 3wf 4841 . 2  F :
-->
53, 1wfn 4840 . . 3  F  Fn
63crn 4289 . . . 4  ran  F
76, 2wss 2911 . . 3  ran  F  C_
85, 7wa 97 . 2  F  Fn  ran  F  C_
94, 8wb 98 1  F : -->  F  Fn  ran  F 
C_
Colors of variables: wff set class
This definition is referenced by:  feq1  4973  feq2  4974  feq3  4975  nff  4986  sbcfg  4988  ffn  4989  dffn2  4990  frn  4995  dffn3  4996  fss  4997  fco  4999  funssxp  5003  fun  5006  fnfco  5008  fssres  5009  fcoi2  5014  fintm  5018  fin  5019  f0  5023  fconst  5025  f1ssr  5041  fof  5049  dff1o2  5074  fun11iun  5090  ffoss  5101  dff2  5254  fmpt  5262  ffnfv  5266  ffvresb  5271  fpr  5288  fprg  5289  idref  5339  dff1o6  5359  fliftf  5382  1stcof  5732  2ndcof  5733  smores  5848  smores2  5850  iordsmo  5853  frec2uzf1od  8853
  Copyright terms: Public domain W3C validator