Definition df-f 5930

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 6411, dff3 6412, and dff4 6413. (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 5922	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5921	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5144	. . . 4 class ran 𝐹
7	6, 2	wss 3607	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 383	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 196	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6064  feq2  6065  feq3  6066  nff  6079  sbcfg  6081  ffn  6083  dffn2  6085  frn  6091  dffn3  6092  fss  6094  fco  6096  funssxp  6099  fdmrn  6102  fun  6104  fnfco  6107  fssres  6108  fcoi2  6117  fint  6122  fin  6123  f0  6124  fconst  6129  f1ssr  6145  fof  6153  dff1o2  6180  dff2  6411  dff3  6412  fmpt  6421  ffnfv  6428  ffvresb  6434  fpr  6461  idref  6539  dff1o6  6571  fliftf  6605  fun11iun  7168  ffoss  7169  1stcof  7240  2ndcof  7241  smores  7494  smores2  7496  iordsmo  7499  sbthlem9  8119  sucdom2  8197  inf3lem6  8568  alephsmo  8963  alephsing  9136  axdc3lem2  9311  smobeth  9446  fpwwe2lem11  9500  gch3  9536  gruiun  9659  gruima  9662  nqerf  9790  om2uzf1oi  12792  fclim  14328  invf  16475  funcres2b  16604  funcres2c  16608  hofcllem  16945  hofcl  16946  gsumval2  17327  resmhm2b  17408  frmdss2  17447  gsumval3a  18350  subgdmdprd  18479  srgfcl  18561  lsslindf  20217  indlcim  20227  cnrest2  21138  lmss  21150  conncn  21277  txflf  21857  cnextf  21917  clsnsg  21960  tgpconncomp  21963  psmetxrge0  22165  causs  23142  ellimc2  23686  perfdvf  23712  c1lip2  23806  dvne0  23819  plyeq0  24012  plyreres  24083  aannenlem1  24128  taylf  24160  ulmss  24196  mptelee  25820  ausgrusgrb  26105  ausgrumgri  26107  usgrexmplef  26196  subuhgr  26223  subupgr  26224  subumgr  26225  subusgr  26226  upgrres  26243  umgrres  26244  hhssnv  28249  pjfi  28691  maprnin  29634  measdivcstOLD  30415  sitgf  30537  eulerpartlemn  30571  reprinrn  30824  cvmlift2lem9a  31411  elno2  31932  elno3  31933  scutf  32044  icoreresf  33330  poimirlem30  33569  poimirlem31  33570  isbnd3  33713  dihf11lem  36872  ntrf  38738  clsf2  38741  gneispace3  38748  gneispacef2  38751  gneispacern  38753  k0004lem1  38762  dvsid  38847  stoweidlem27  40562  stoweidlem29  40564  stoweidlem31  40566  fourierdlem15  40657  mbfresmf  41269  ffnafv  41572  iccpartf  41692  resmgmhm2b  42125