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

Definition df-f 4973
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 : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3wf 4965 . 2  wff  F : A
--> B
53, 1wfn 4964 . . 3  wff  F  Fn  A
63crn 4402 . . . 4  class  ran  F
76, 2wss 2984 . . 3  wff  ran  F  C_  B
85, 7wa 102 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 103 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff set class
This definition is referenced by:  feq1  5098  feq2  5099  feq3  5100  nff  5111  sbcfg  5113  ffn  5114  dffn2  5116  frn  5121  dffn3  5122  fss  5123  fco  5125  funssxp  5129  fun  5132  fnfco  5134  fssres  5135  fcoi2  5140  fintm  5144  fin  5145  f0  5149  fconst  5154  f1ssr  5171  fof  5181  dff1o2  5206  fun11iun  5222  ffoss  5233  dff2  5388  fmpt  5394  ffnfv  5398  ffvresb  5403  fpr  5421  fprg  5422  idref  5476  dff1o6  5495  fliftf  5518  1stcof  5869  2ndcof  5870  smores  5989  smores2  5991  iordsmo  5994  tfrcllembfn  6054  inresflem  6659  frec2uzf1od  9702  frecuzrdgtcl  9708  fclim  10507  nninfall  11241
  Copyright terms: Public domain W3C validator