Definition df-f 6186

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. 𝐹:𝐴⟶𝐵 can be read as "𝐹 is a function from 𝐴 to 𝐵". For alternate definitions, see dff2 6682, dff3 6683, and dff4 6684. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f	⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf 6178	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6177	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5401	. . . 4 class ran 𝐹
7	6, 2	wss 3825	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 387	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 198	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6319  feq2  6320  feq3  6321  nff  6334  sbcfg  6336  ffn  6338  dffn2  6340  frn  6344  dffn3  6349  fss  6351  fco  6355  funssxp  6358  fdmrn  6361  fun  6363  fnfco  6366  fssres  6367  fcoi2  6376  fint  6381  fin  6382  f0  6383  fconst  6388  f1ssr  6404  fof  6413  dff1o2  6443  dff2  6682  dff3  6683  fmpt  6691  ffnfv  6699  ffvresb  6705  idref  6725  fpr  6733  dff1o6  6851  fliftf  6885  fun11iun  7452  ffoss  7453  1stcof  7524  2ndcof  7525  smores  7786  smores2  7788  iordsmo  7791  sbthlem9  8423  inf3lem6  8882  alephsmo  9314  alephsing  9488  axdc3lem2  9663  smobeth  9798  fpwwe2lem11  9852  gruiun  10011  gruima  10014  nqerf  10142  om2uzf1oi  13129  fclim  14761  invf  16886  funcres2b  17015  funcres2c  17019  hofcllem  17356  hofcl  17357  gsumval2  17738  resmhm2b  17819  frmdss2  17859  gsumval3a  18767  subgdmdprd  18896  srgfcl  18978  lsslindf  20666  indlcim  20676  cnrest2  21588  lmss  21600  conncn  21728  txflf  22308  cnextf  22368  clsnsg  22411  tgpconncomp  22414  psmetxrge0  22616  causs  23594  ellimc2  24168  perfdvf  24194  c1lip2  24288  dvne0  24301  plyeq0  24494  plyreres  24565  aannenlem1  24610  taylf  24642  ulmss  24678  mptelee  26374  ausgrusgrb  26643  ausgrumgri  26645  usgrexmplef  26734  subuhgr  26761  subupgr  26762  subumgr  26763  subusgr  26764  upgrres  26781  umgrres  26782  hhssnv  28810  pjfi  29252  maprnin  30208  measdivcstOLD  31085  sitgf  31207  eulerpartlemn  31241  reprinrn  31498  cvmlift2lem9a  32095  elno2  32622  elno3  32623  scutf  32734  icoreresf  34010  poimirlem30  34311  poimirlem31  34312  isbnd3  34452  dihf11lem  37795  ntrf  39781  clsf2  39784  gneispace3  39791  gneispacef2  39794  k0004lem1  39805  dvsid  40023  stoweidlem27  41689  stoweidlem29  41691  stoweidlem31  41693  fourierdlem15  41784  mbfresmf  42393  ffnafv  42722  frnvafv2v  42787  iccpartf  42909  resmgmhm2b  43375