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

Definition df-f 4930
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 4922 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 4921 . . 3 wff 𝐹 Fn 𝐴
63crn 4366 . . . 4 class ran 𝐹
76, 2wss 2974 . . 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  5055  feq2  5056  feq3  5057  nff  5068  sbcfg  5070  ffn  5071  dffn2  5072  frn  5077  dffn3  5078  fss  5079  fco  5081  funssxp  5085  fun  5088  fnfco  5090  fssres  5091  fcoi2  5096  fintm  5100  fin  5101  f0  5105  fconst  5107  f1ssr  5123  fof  5131  dff1o2  5156  fun11iun  5172  ffoss  5183  dff2  5337  fmpt  5345  ffnfv  5349  ffvresb  5354  fpr  5371  fprg  5372  idref  5422  dff1o6  5441  fliftf  5464  1stcof  5815  2ndcof  5816  smores  5935  smores2  5937  iordsmo  5940  tfrcllembfn  6000  frec2uzf1od  9477  frecuzrdgtcl  9483  fclim  10260
  Copyright terms: Public domain W3C validator