Definition df-f 6541

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 7095, dff3 7096, and dff4 7097. (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 6533	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6532	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5660	. . . 4 class ran 𝐹
7	6, 2	wss 3902	. . 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  6684  feq2  6685  feq3  6686  nff  6702  sbcfg  6704  ffn  6706  dffn2  6708  frn  6714  dffn3  6719  ffrnb  6721  fss  6723  fcof  6730  funssxp  6735  fdmrn  6738  fun  6741  fnfco  6744  fssres  6745  fcoi2  6754  fint  6758  fin  6759  f0  6760  fconst  6765  f1ssr  6783  fof  6793  dff1o2  6827  dff2  7095  dff3  7096  fmpt  7106  ffnfv  7115  ffvresb  7122  idref  7145  fpr  7154  dff1o6  7279  fliftf  7319  fiun  7943  f1iun  7944  ffoss  7946  1stcof  8019  2ndcof  8020  smores  8344  smores2  8346  iordsmo  8349  sbthlem9  9096  inf3lem6  9615  alephsmo  10108  alephsing  10281  axdc3lem2  10456  smobeth  10598  fpwwe2lem10  10652  gruiun  10811  gruima  10814  nqerf  10942  om2uzf1oi  14019  fclim  15642  invf  17861  funcres2b  17990  funcres2c  17996  hofcllem  18350  hofcl  18351  nfchnd  18703  mgmn0plusgf  18745  gsumval2  18790  resmgmhm2b  18817  resmhm2b  18932  frmdss2  18973  gsumval3a  20031  subgdmdprd  20164  srgfcl  20336  lsslindf  22044  indlcim  22054  cnrest2  23512  lmss  23524  conncn  23652  txflf  24233  cnextf  24293  clsnsg  24337  tgpconncomp  24340  psmetxrge0  24540  causs  25527  ellimc2  26106  perfdvf  26132  c1lip2  26227  dvne0  26240  plyeq0  26438  plyreres  26514  aannenlem1  26561  taylf  26594  ulmss  26630  elno2  27888  elno3  27889  cutsf  28055  madef  28099  oniso  28534  mpteleeOLD  29338  ausgrusgrb  29611  ausgrumgri  29613  usgrexmplef  29705  subuhgr  29732  subupgr  29733  subumgr  29734  subusgr  29735  upgrres  29752  umgrres  29753  hhssnv  31731  pjfi  32171  maprnin  33189  cycpmconjslem1  33581  esplyfv1  34066  measdivcstALTV  34723  sitgf  34845  eulerpartlemn  34879  reprinrn  35113  cvmlift2lem9a  35869  satff  35976  icoreresf  38093  poimirlem30  38386  poimirlem31  38387  isbnd3  38521  dihf11lem  42126  ofoafg  44182  ofoaid1  44186  ofoaid2  44187  naddcnff  44190  ntrf  44950  clsf2  44953  gneispace3  44960  gneispacef2  44963  k0004lem1  44974  dvsid  45142  stoweidlem27  46842  stoweidlem29  46844  stoweidlem31  46846  fourierdlem15  46937  mbfresmf  47554  ffnafv  48046  fcdmvafv2v  48111  iccpartf  48318  slotresfo  49812