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

Definition df-f 5220
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 5212 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 5211 . . 3 wff 𝐹 Fn 𝐴
63crn 4627 . . . 4 class ran 𝐹
76, 2wss 3129 . . 3 wff ran 𝐹𝐵
85, 7wa 104 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 105 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
Colors of variables: wff set class
This definition is referenced by:  feq1  5348  feq2  5349  feq3  5350  nff  5362  sbcfg  5364  ffn  5365  dffn2  5367  frn  5374  dffn3  5376  fss  5377  fco  5381  funssxp  5385  fun  5388  fnfco  5390  fssres  5391  fcoi2  5397  fintm  5401  fin  5402  f0  5406  fconst  5411  f1ssr  5428  fof  5438  dff1o2  5466  fun11iun  5482  ffoss  5493  dff2  5660  fmpt  5666  ffnfv  5674  ffvresb  5679  fpr  5698  fprg  5699  idref  5757  dff1o6  5776  fliftf  5799  1stcof  6163  2ndcof  6164  smores  6292  smores2  6294  iordsmo  6297  tfrcllembfn  6357  sbthlemi9  6963  inresflem  7058  frec2uzf1od  10405  frecuzrdgtcl  10411  fclim  11301  ennnfonelemf1  12418  srgfcl  13154  cnrest2  13706  lmss  13716  psmetxrge0  13802  dvfgg  14127  nninfall  14728
  Copyright terms: Public domain W3C validator