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

Definition df-f 5097
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 5089 . 2  wff  F : A
--> B
53, 1wfn 5088 . . 3  wff  F  Fn  A
63crn 4510 . . . 4  class  ran  F
76, 2wss 3041 . . 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  5225  feq2  5226  feq3  5227  nff  5239  sbcfg  5241  ffn  5242  dffn2  5244  frn  5251  dffn3  5253  fss  5254  fco  5258  funssxp  5262  fun  5265  fnfco  5267  fssres  5268  fcoi2  5274  fintm  5278  fin  5279  f0  5283  fconst  5288  f1ssr  5305  fof  5315  dff1o2  5340  fun11iun  5356  ffoss  5367  dff2  5532  fmpt  5538  ffnfv  5546  ffvresb  5551  fpr  5570  fprg  5571  idref  5626  dff1o6  5645  fliftf  5668  1stcof  6029  2ndcof  6030  smores  6157  smores2  6159  iordsmo  6162  tfrcllembfn  6222  sbthlemi9  6821  inresflem  6913  frec2uzf1od  10134  frecuzrdgtcl  10140  fclim  11018  ennnfonelemf1  11842  cnrest2  12316  lmss  12326  psmetxrge0  12412  dvfgg  12737  nninfall  13100
  Copyright terms: Public domain W3C validator