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

Definition df-f 5187
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 5179 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 5178 . . 3 wff 𝐹 Fn 𝐴
63crn 4600 . . . 4 class ran 𝐹
76, 2wss 3112 . . 3 wff ran 𝐹𝐵
85, 7wa 103 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 104 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
Colors of variables: wff set class
This definition is referenced by:  feq1  5315  feq2  5316  feq3  5317  nff  5329  sbcfg  5331  ffn  5332  dffn2  5334  frn  5341  dffn3  5343  fss  5344  fco  5348  funssxp  5352  fun  5355  fnfco  5357  fssres  5358  fcoi2  5364  fintm  5368  fin  5369  f0  5373  fconst  5378  f1ssr  5395  fof  5405  dff1o2  5432  fun11iun  5448  ffoss  5459  dff2  5624  fmpt  5630  ffnfv  5638  ffvresb  5643  fpr  5662  fprg  5663  idref  5720  dff1o6  5739  fliftf  5762  1stcof  6124  2ndcof  6125  smores  6252  smores2  6254  iordsmo  6257  tfrcllembfn  6317  sbthlemi9  6922  inresflem  7017  frec2uzf1od  10332  frecuzrdgtcl  10338  fclim  11225  ennnfonelemf1  12314  cnrest2  12803  lmss  12813  psmetxrge0  12899  dvfgg  13224  nninfall  13750
  Copyright terms: Public domain W3C validator