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

Definition df-f 4933
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 4925 . 2  wff  F : A
--> B
53, 1wfn 4924 . . 3  wff  F  Fn  A
63crn 4373 . . . 4  class  ran  F
76, 2wss 2944 . . 3  wff  ran  F  C_  B
85, 7wa 101 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 102 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff set class
This definition is referenced by:  feq1  5057  feq2  5058  feq3  5059  nff  5070  sbcfg  5072  ffn  5073  dffn2  5074  frn  5079  dffn3  5080  fss  5081  fco  5083  funssxp  5087  fun  5090  fnfco  5092  fssres  5093  fcoi2  5098  fintm  5102  fin  5103  f0  5107  fconst  5109  f1ssr  5125  fof  5133  dff1o2  5158  fun11iun  5174  ffoss  5185  dff2  5338  fmpt  5346  ffnfv  5350  ffvresb  5355  fpr  5372  fprg  5373  idref  5423  dff1o6  5443  fliftf  5466  1stcof  5817  2ndcof  5818  smores  5937  smores2  5939  iordsmo  5942  frec2uzf1od  9355  fclim  10045
  Copyright terms: Public domain W3C validator