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

Definition df-f 4987
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 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3wf 4979 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 4978 . . 3 wff 𝐹 Fn 𝐴
63crn 4414 . . . 4 class ran 𝐹
76, 2wss 2988 . . 3 wff ran 𝐹𝐵
85, 7wa 102 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 103 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
Colors of variables: wff set class
This definition is referenced by:  feq1  5112  feq2  5113  feq3  5114  nff  5125  sbcfg  5127  ffn  5128  dffn2  5130  frn  5136  dffn3  5137  fss  5138  fco  5142  funssxp  5146  fun  5149  fnfco  5151  fssres  5152  fcoi2  5157  fintm  5161  fin  5162  f0  5166  fconst  5171  f1ssr  5188  fof  5198  dff1o2  5223  fun11iun  5239  ffoss  5250  dff2  5408  fmpt  5414  ffnfv  5421  ffvresb  5426  fpr  5444  fprg  5445  idref  5499  dff1o6  5518  fliftf  5541  1stcof  5893  2ndcof  5894  smores  6013  smores2  6015  iordsmo  6018  tfrcllembfn  6078  sbthlemi9  6621  inresflem  6699  frec2uzf1od  9744  frecuzrdgtcl  9750  fclim  10580  nninfall  11369
  Copyright terms: Public domain W3C validator