Definition df-f 6527

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 7082, dff3 7083, and dff4 7084. (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 6519	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6518	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5650	. . . 4 class ran 𝐹
7	6, 2	wss 3906	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 399	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 208	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6671  feq2  6672  feq3  6673  nff  6689  sbcfg  6691  ffn  6693  dffn2  6695  frn  6701  dffn3  6706  ffrnb  6708  fss  6710  fcof  6717  funssxp  6722  fdmrn  6725  fun  6728  fnfco  6731  fssres  6732  fcoi2  6741  fint  6745  fin  6746  f0  6747  fconst  6752  f1ssr  6770  fof  6780  dff1o2  6814  dff2  7082  dff3  7083  fmpt  7093  ffnfv  7102  ffvresb  7109  idref  7130  fpr  7139  dff1o6  7261  fliftf  7301  fiun  7926  f1iun  7927  ffoss  7929  1stcof  8002  2ndcof  8003  smores  8325  smores2  8327  iordsmo  8330  sbthlem9  9069  inf3lem6  9590  alephsmo  10060  alephsing  10235  axdc3lem2  10410  smobeth  10546  fpwwe2lem10  10600  gruiun  10759  gruima  10762  nqerf  10890  om2uzf1oi  13968  fclim  15582  invf  17803  funcres2b  17932  funcres2c  17938  hofcllem  18292  hofcl  18293  nfchnd  18645  gsumval2  18722  resmgmhm2b  18749  resmhm2b  18858  frmdss2  18899  gsumval3a  19945  subgdmdprd  20078  srgfcl  20248  lsslindf  21884  indlcim  21894  cnrest2  23348  lmss  23360  conncn  23488  txflf  24068  cnextf  24128  clsnsg  24172  tgpconncomp  24175  psmetxrge0  24375  causs  25362  ellimc2  25941  perfdvf  25967  c1lip2  26062  dvne0  26075  plyeq0  26273  plyreres  26349  aannenlem1  26394  taylf  26426  ulmss  26462  elno2  27720  elno3  27721  cutsf  27887  madef  27931  oniso  28366  mpteleeOLD  29098  ausgrusgrb  29368  ausgrumgri  29370  usgrexmplef  29462  subuhgr  29489  subupgr  29490  subumgr  29491  subusgr  29492  upgrres  29509  umgrres  29510  hhssnv  31469  pjfi  31909  maprnin  32935  cycpmconjslem1  33336  esplyfv1  33868  measdivcstALTV  34524  sitgf  34646  eulerpartlemn  34680  reprinrn  34914  cvmlift2lem9a  35658  satff  35765  icoreresf  37851  poimirlem30  38154  poimirlem31  38155  isbnd3  38288  dihf11lem  41895  ofoafg  43936  ofoaid1  43940  ofoaid2  43941  naddcnff  43944  ntrf  44704  clsf2  44707  gneispace3  44714  gneispacef2  44717  k0004lem1  44728  dvsid  44912  stoweidlem27  46606  stoweidlem29  46608  stoweidlem31  46610  fourierdlem15  46701  mbfresmf  47318  sinnpoly  47490  ffnafv  47770  fcdmvafv2v  47835  iccpartf  48042  slotresfo  49525