Definition df-f 6540

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 7094, dff3 7095, and dff4 7096. (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 6532	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6531	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5661	. . . 4 class ran 𝐹
7	6, 2	wss 3904	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 400	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is used by:  feq1  6683  feq2  6684  feq3  6685  nff  6701  sbcfg  6703  ffn  6705  dffn2  6707  frn  6713  dffn3  6718  ffrnb  6720  fss  6722  fcof  6729  funssxp  6734  fdmrn  6737  fun  6740  fnfco  6743  fssres  6744  fcoi2  6753  fint  6757  fin  6758  f0  6759  fconst  6764  f1ssr  6782  fof  6792  dff1o2  6826  dff2  7094  dff3  7095  fmpt  7105  ffnfv  7114  ffvresb  7121  idref  7142  fpr  7151  dff1o6  7273  fliftf  7313  fiun  7938  f1iun  7939  ffoss  7941  1stcof  8014  2ndcof  8015  smores  8337  smores2  8339  iordsmo  8342  sbthlem9  9081  inf3lem6  9600  alephsmo  10093  alephsing  10266  axdc3lem2  10441  smobeth  10577  fpwwe2lem10  10631  gruiun  10790  gruima  10793  nqerf  10921  om2uzf1oi  13996  fclim  15611  invf  17831  funcres2b  17960  funcres2c  17966  hofcllem  18320  hofcl  18321  nfchnd  18673  gsumval2  18750  resmgmhm2b  18777  resmhm2b  18887  frmdss2  18928  gsumval3a  19979  subgdmdprd  20112  srgfcl  20284  lsslindf  21991  indlcim  22001  cnrest2  23454  lmss  23466  conncn  23594  txflf  24174  cnextf  24234  clsnsg  24278  tgpconncomp  24281  psmetxrge0  24481  causs  25468  ellimc2  26047  perfdvf  26073  c1lip2  26168  dvne0  26181  plyeq0  26379  plyreres  26455  aannenlem1  26502  taylf  26535  ulmss  26571  elno2  27829  elno3  27830  cutsf  27996  madef  28040  oniso  28475  mpteleeOLD  29256  ausgrusgrb  29526  ausgrumgri  29528  usgrexmplef  29620  subuhgr  29647  subupgr  29648  subumgr  29649  subusgr  29650  upgrres  29667  umgrres  29668  hhssnv  31627  pjfi  32067  maprnin  33087  cycpmconjslem1  33483  esplyfv1  33968  measdivcstALTV  34624  sitgf  34746  eulerpartlemn  34780  reprinrn  35014  cvmlift2lem9a  35803  satff  35910  icoreresf  38026  poimirlem30  38329  poimirlem31  38330  isbnd3  38463  dihf11lem  42068  ofoafg  44109  ofoaid1  44113  ofoaid2  44114  naddcnff  44117  ntrf  44877  clsf2  44880  gneispace3  44887  gneispacef2  44890  k0004lem1  44901  dvsid  45069  stoweidlem27  46769  stoweidlem29  46771  stoweidlem31  46773  fourierdlem15  46864  mbfresmf  47481  sinnpoly  47656  ffnafv  47936  fcdmvafv2v  48001  iccpartf  48208  slotresfo  49705