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

Definition df-f 5134
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 5126 . 2  wff  F : A
--> B
53, 1wfn 5125 . . 3  wff  F  Fn  A
63crn 4547 . . . 4  class  ran  F
76, 2wss 3075 . . 3  wff  ran  F  C_  B
85, 7wa 103 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 104 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff set class
This definition is referenced by:  feq1  5262  feq2  5263  feq3  5264  nff  5276  sbcfg  5278  ffn  5279  dffn2  5281  frn  5288  dffn3  5290  fss  5291  fco  5295  funssxp  5299  fun  5302  fnfco  5304  fssres  5305  fcoi2  5311  fintm  5315  fin  5316  f0  5320  fconst  5325  f1ssr  5342  fof  5352  dff1o2  5379  fun11iun  5395  ffoss  5406  dff2  5571  fmpt  5577  ffnfv  5585  ffvresb  5590  fpr  5609  fprg  5610  idref  5665  dff1o6  5684  fliftf  5707  1stcof  6068  2ndcof  6069  smores  6196  smores2  6198  iordsmo  6201  tfrcllembfn  6261  sbthlemi9  6860  inresflem  6952  frec2uzf1od  10209  frecuzrdgtcl  10215  fclim  11094  ennnfonelemf1  11965  cnrest2  12442  lmss  12452  psmetxrge0  12538  dvfgg  12863  nninfall  13377
  Copyright terms: Public domain W3C validator