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

Definition df-f 4829
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 (𝐹:AB ↔ (𝐹 Fn A ran 𝐹B))

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cF . . 3 class 𝐹
41, 2, 3wf 4821 . 2 wff 𝐹:AB
53, 1wfn 4820 . . 3 wff 𝐹 Fn A
63crn 4269 . . . 4 class ran 𝐹
76, 2wss 2890 . . 3 wff ran 𝐹B
85, 7wa 97 . 2 wff (𝐹 Fn A ran 𝐹B)
94, 8wb 98 1 wff (𝐹:AB ↔ (𝐹 Fn A ran 𝐹B))
Colors of variables: wff set class
This definition is referenced by:  feq1  4952  feq2  4953  feq3  4954  nff  4965  sbcfg  4967  ffn  4968  dffn2  4969  frn  4974  dffn3  4975  fss  4976  fco  4977  funssxp  4981  fun  4984  fnfco  4986  fssres  4987  fcoi2  4992  fintm  4996  fin  4997  f0  5001  fconst  5003  f1ssr  5019  fof  5027  dff1o2  5052  fun11iun  5068  ffoss  5079  dff2  5232  fmpt  5240  ffnfv  5244  ffvresb  5249  fpr  5266  fprg  5267  idref  5317  dff1o6  5337  fliftf  5360  1stcof  5709  2ndcof  5710  smores  5825  smores2  5827  iordsmo  5830
  Copyright terms: Public domain W3C validator