Definition df-f 6485

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 7032, dff3 7033, and dff4 7034. (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 6477	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6476	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5615	. . . 4 class ran 𝐹
7	6, 2	wss 3897	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 395	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 206	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6629  feq2  6630  feq3  6631  nff  6647  sbcfg  6649  ffn  6651  dffn2  6653  frn  6658  dffn3  6663  ffrnb  6665  fss  6667  fcof  6674  funssxp  6679  fdmrn  6682  fun  6685  fnfco  6688  fssres  6689  fcoi2  6698  fint  6702  fin  6703  f0  6704  fconst  6709  f1ssr  6725  fof  6735  dff1o2  6768  dff2  7032  dff3  7033  fmpt  7043  ffnfv  7052  ffvresb  7058  idref  7079  fpr  7087  dff1o6  7209  fliftf  7249  fiun  7875  f1iun  7876  ffoss  7878  1stcof  7951  2ndcof  7952  smores  8272  smores2  8274  iordsmo  8277  sbthlem9  9008  inf3lem6  9523  alephsmo  9993  alephsing  10167  axdc3lem2  10342  smobeth  10477  fpwwe2lem10  10531  gruiun  10690  gruima  10693  nqerf  10821  om2uzf1oi  13860  fclim  15460  invf  17675  funcres2b  17804  funcres2c  17810  hofcllem  18164  hofcl  18165  nfchnd  18517  gsumval2  18594  resmgmhm2b  18621  resmhm2b  18730  frmdss2  18771  gsumval3a  19815  subgdmdprd  19948  srgfcl  20114  lsslindf  21767  indlcim  21777  cnrest2  23201  lmss  23213  conncn  23341  txflf  23921  cnextf  23981  clsnsg  24025  tgpconncomp  24028  psmetxrge0  24228  causs  25225  ellimc2  25805  perfdvf  25831  c1lip2  25930  dvne0  25943  plyeq0  26143  plyreres  26217  aannenlem1  26263  taylf  26295  ulmss  26333  elno2  27593  elno3  27594  scutf  27753  madef  27797  onsiso  28205  mptelee  28873  ausgrusgrb  29143  ausgrumgri  29145  usgrexmplef  29237  subuhgr  29264  subupgr  29265  subumgr  29266  subusgr  29267  upgrres  29284  umgrres  29285  hhssnv  31244  pjfi  31684  maprnin  32714  cycpmconjslem1  33123  esplyfv1  33590  measdivcstALTV  34238  sitgf  34360  eulerpartlemn  34394  reprinrn  34631  cvmlift2lem9a  35347  satff  35454  icoreresf  37394  poimirlem30  37698  poimirlem31  37699  isbnd3  37832  dihf11lem  41313  ofoafg  43395  ofoaid1  43399  ofoaid2  43400  naddcnff  43403  ntrf  44164  clsf2  44167  gneispace3  44174  gneispacef2  44177  k0004lem1  44188  dvsid  44372  stoweidlem27  46073  stoweidlem29  46075  stoweidlem31  46077  fourierdlem15  46168  mbfresmf  46785  sinnpoly  46930  ffnafv  47210  fcdmvafv2v  47275  iccpartf  47470  slotresfo  48938