Definition df-f 6542

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 7099, dff3 7100, and dff4 7101. (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 6534	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6533	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5651	. . . 4 class ran 𝐹
7	6, 2	wss 3895	. . 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  6687  feq2  6688  feq3  6689  nff  6705  sbcfg  6707  ffn  6709  dffn2  6711  frn  6717  dffn3  6722  ffrnb  6724  fss  6726  fcof  6733  funssxp  6738  fdmrn  6741  fun  6744  fnfco  6747  fssres  6748  fcoi2  6757  fint  6761  fin  6762  f0  6763  fconst  6768  f1ssr  6786  fof  6796  dff1o2  6830  dff2  7099  dff3  7100  fmpt  7110  ffnfv  7119  ffvresb  7126  idref  7149  fpr  7158  dff1o6  7283  fliftf  7323  fiun  7955  f1iun  7956  ffoss  7958  1stcof  8031  2ndcof  8032  smores  8360  smores2  8362  iordsmo  8365  sbthlem9  9114  inf3lem6  9634  alephsmo  10181  alephsing  10354  axdc3lem2  10529  smobeth  10671  fpwwe2lem10  10725  gruiun  10884  gruima  10887  nqerf  11015  om2uzf1oi  14096  fclim  15720  invf  17943  funcres2b  18072  funcres2c  18078  hofcllem  18432  hofcl  18433  nfchnd  18785  mgmn0plusgf  18827  gsumval2  18875  resmgmhm2b  18902  resmhm2b  19018  frmdss2  19059  gsumval3a  20117  subgdmdprd  20250  srgfcl  20422  lsslindf  22136  indlcim  22146  cnrest2  23604  lmss  23616  conncn  23744  txflf  24325  cnextf  24385  clsnsg  24429  tgpconncomp  24432  psmetxrge0  24632  causs  25619  ellimc2  26197  perfdvf  26223  c1lip2  26318  dvne0  26331  plyeq0  26530  plyreres  26604  aannenlem1  26655  taylf  26688  ulmss  26724  elno2  28011  elno3  28012  cutsf  28178  madef  28222  oniso  28657  mpteleeOLD  29473  ausgrusgrb  29746  ausgrumgri  29748  usgrexmplef  29840  subuhgr  29867  subupgr  29868  subumgr  29869  subusgr  29870  upgrres  29887  umgrres  29888  hhssnv  31866  pjfi  32306  maprnin  33365  cycpmconjslem1  33757  esplyfv1  34243  measdivcstALTV  34900  sitgf  35021  eulerpartlemn  35055  reprinrn  35289  cvmlift2lem9a  36110  satff  36217  icoreresf  38318  poimirlem30  38611  poimirlem31  38612  isbnd3  38761  dihf11lem  42366  ofoafg  44398  ofoaid1  44402  ofoaid2  44403  naddcnff  44406  ntrf  45165  clsf2  45168  gneispace3  45175  gneispacef2  45178  k0004lem1  45189  dvsid  45357  stoweidlem27  47079  stoweidlem29  47081  stoweidlem31  47083  fourierdlem15  47174  mbfresmf  47791  ffnafv  48283  fcdmvafv2v  48348  iccpartf  48555  slotresfo  50049