Definition df-f 6559

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 7120, dff3 7121, and dff4 7122. (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 6551	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6550	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5656	. . . 4 class ran 𝐹
7	6, 2	wss 3900	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 401	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is used by:  feq1  6706  feq2  6707  feq3  6708  nff  6724  sbcfg  6726  ffn  6728  dffn2  6730  frn  6736  dffn3  6741  ffrnb  6743  fss  6745  fcof  6752  funssxp  6757  fdmrn  6760  fun  6763  fnfco  6766  fssres  6767  fcoi2  6776  fint  6780  fin  6781  f0  6782  fconst  6787  f1ssr  6805  fof  6815  dff1o2  6849  dff2  7120  dff3  7121  fmpt  7131  ffnfv  7140  ffvresb  7147  idref  7170  fpr  7179  dff1o6  7303  fliftf  7343  fiun  7976  f1iun  7977  ffoss  7979  1stcof  8052  2ndcof  8053  smores  8385  smores2  8387  iordsmo  8390  sbthlem9  9139  inf3lem6  9658  alephsmo  10205  alephsing  10378  axdc3lem2  10553  smobeth  10695  fpwwe2lem10  10749  gruiun  10908  gruima  10911  nqerf  11039  om2uzf1oi  14120  fclim  15746  invf  17969  funcres2b  18098  funcres2c  18104  hofcllem  18458  hofcl  18459  nfchnd  18811  mgmn0plusgf  18853  gsumval2  18901  resmgmhm2b  18928  resmhm2b  19044  frmdss2  19085  gsumval3a  20144  subgdmdprd  20277  srgfcl  20449  lsslindf  22163  indlcim  22173  cnrest2  23631  lmss  23643  conncn  23771  txflf  24352  cnextf  24412  clsnsg  24456  tgpconncomp  24459  psmetxrge0  24659  causs  25646  ellimc2  26224  perfdvf  26250  c1lip2  26345  dvne0  26358  plyeq0  26557  plyreres  26631  aannenlem1  26682  taylf  26715  ulmss  26751  elno2  28038  elno3  28039  cutsf  28205  madef  28249  oniso  28684  mpteleeOLD  29500  ausgrusgrb  29773  ausgrumgri  29775  usgrexmplef  29867  subuhgr  29894  subupgr  29895  subumgr  29896  subusgr  29897  upgrres  29914  umgrres  29915  hhssnv  31893  pjfi  32333  maprnin  33390  cycpmconjslem1  33782  esplyfv1  34268  measdivcstALTV  34925  sitgf  35046  eulerpartlemn  35080  reprinrn  35314  cvmlift2lem9a  36234  satff  36341  icoreresf  38466  poimirlem30  38759  poimirlem31  38760  isbnd3  38909  dihf11lem  42514  ofoafg  44546  ofoaid1  44550  ofoaid2  44551  naddcnff  44554  ntrf  45313  clsf2  45316  gneispace3  45323  gneispacef2  45326  k0004lem1  45337  dvsid  45505  stoweidlem27  47240  stoweidlem29  47242  stoweidlem31  47244  fourierdlem15  47335  mbfresmf  47952  ffnafv  48444  fcdmvafv2v  48509  iccpartf  48716  slotresfo  50216