Definition df-f 6577

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 7133, dff3 7134, and dff4 7135. (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 6569	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6568	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5701	. . . 4 class ran 𝐹
7	6, 2	wss 3976	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 395	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 206	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6728  feq2  6729  feq3  6730  nff  6743  sbcfg  6745  ffn  6747  dffn2  6749  frn  6754  dffn3  6759  ffrnb  6761  fss  6763  fcof  6770  fcoOLD  6772  funssxp  6776  fdmrn  6779  fun  6783  fnfco  6786  fssres  6787  fcoi2  6796  fint  6800  fin  6801  f0  6802  fconst  6807  f1ssr  6823  fof  6834  dff1o2  6867  dff2  7133  dff3  7134  fmpt  7144  ffnfv  7153  ffvresb  7159  idref  7180  fpr  7188  dff1o6  7311  fliftf  7351  fiun  7983  f1iun  7984  ffoss  7986  1stcof  8060  2ndcof  8061  smores  8408  smores2  8410  iordsmo  8413  sbthlem9  9157  inf3lem6  9702  alephsmo  10171  alephsing  10345  axdc3lem2  10520  smobeth  10655  fpwwe2lem10  10709  gruiun  10868  gruima  10871  nqerf  10999  om2uzf1oi  14004  fclim  15599  invf  17829  funcres2b  17961  funcres2c  17968  hofcllem  18328  hofcl  18329  gsumval2  18724  resmgmhm2b  18751  resmhm2b  18857  frmdss2  18898  gsumval3a  19945  subgdmdprd  20078  srgfcl  20223  lsslindf  21873  indlcim  21883  cnrest2  23315  lmss  23327  conncn  23455  txflf  24035  cnextf  24095  clsnsg  24139  tgpconncomp  24142  psmetxrge0  24344  causs  25351  ellimc2  25932  perfdvf  25958  c1lip2  26057  dvne0  26070  plyeq0  26270  plyreres  26342  aannenlem1  26388  taylf  26420  ulmss  26458  elno2  27717  elno3  27718  scutf  27875  madef  27913  mptelee  28928  ausgrusgrb  29200  ausgrumgri  29202  usgrexmplef  29294  subuhgr  29321  subupgr  29322  subumgr  29323  subusgr  29324  upgrres  29341  umgrres  29342  hhssnv  31296  pjfi  31736  maprnin  32745  cycpmconjslem1  33147  measdivcstALTV  34189  sitgf  34312  eulerpartlemn  34346  reprinrn  34595  cvmlift2lem9a  35271  satff  35378  icoreresf  37318  poimirlem30  37610  poimirlem31  37611  isbnd3  37744  dihf11lem  41223  ofoafg  43316  ofoaid1  43320  ofoaid2  43321  naddcnff  43324  ntrf  44085  clsf2  44088  gneispace3  44095  gneispacef2  44098  k0004lem1  44109  dvsid  44300  stoweidlem27  45948  stoweidlem29  45950  stoweidlem31  45952  fourierdlem15  46043  mbfresmf  46660  ffnafv  47086  fcdmvafv2v  47151  iccpartf  47305