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

Definition df-f 4985
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 4977 . 2  wff  F : A
--> B
53, 1wfn 4976 . . 3  wff  F  Fn  A
63crn 4412 . . . 4  class  ran  F
76, 2wss 2988 . . 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  5110  feq2  5111  feq3  5112  nff  5123  sbcfg  5125  ffn  5126  dffn2  5128  frn  5134  dffn3  5135  fss  5136  fco  5140  funssxp  5144  fun  5147  fnfco  5149  fssres  5150  fcoi2  5155  fintm  5159  fin  5160  f0  5164  fconst  5169  f1ssr  5186  fof  5196  dff1o2  5221  fun11iun  5237  ffoss  5248  dff2  5406  fmpt  5412  ffnfv  5419  ffvresb  5424  fpr  5442  fprg  5443  idref  5497  dff1o6  5516  fliftf  5539  1stcof  5891  2ndcof  5892  smores  6011  smores2  6013  iordsmo  6016  tfrcllembfn  6076  sbthlemi9  6618  inresflem  6696  frec2uzf1od  9741  frecuzrdgtcl  9747  fclim  10577  nninfall  11345
  Copyright terms: Public domain W3C validator