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

Definition df-f 5239
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 5231 . 2  wff  F : A
--> B
53, 1wfn 5230 . . 3  wff  F  Fn  A
63crn 4645 . . . 4  class  ran  F
76, 2wss 3144 . . 3  wff  ran  F  C_  B
85, 7wa 104 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 105 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff set class
This definition is referenced by:  feq1  5367  feq2  5368  feq3  5369  nff  5381  sbcfg  5383  ffn  5384  dffn2  5386  frn  5393  dffn3  5395  fss  5396  fco  5400  funssxp  5404  fun  5407  fnfco  5409  fssres  5410  fcoi2  5416  fintm  5420  fin  5421  f0  5425  fconst  5430  f1ssr  5447  fof  5457  dff1o2  5485  fun11iun  5501  ffoss  5512  dff2  5681  fmpt  5687  ffnfv  5695  ffvresb  5700  fpr  5719  fprg  5720  idref  5778  dff1o6  5798  fliftf  5821  1stcof  6189  2ndcof  6190  smores  6318  smores2  6320  iordsmo  6323  tfrcllembfn  6383  sbthlemi9  6995  inresflem  7090  frec2uzf1od  10439  frecuzrdgtcl  10445  fclim  11337  ennnfonelemf1  12472  resmhm2b  12956  srgfcl  13344  cnrest2  14213  lmss  14223  psmetxrge0  14309  dvfgg  14634  nninfall  15237
  Copyright terms: Public domain W3C validator