Definition df-f 5892

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 6371, dff3 6372, and dff4 6373. (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 5884	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5883	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5115	. . . 4 class ran 𝐹
7	6, 2	wss 3574	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 384	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 196	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6026  feq2  6027  feq3  6028  nff  6041  sbcfg  6043  ffn  6045  dffn2  6047  frn  6053  dffn3  6054  fss  6056  fco  6058  funssxp  6061  fdmrn  6064  fun  6066  fnfco  6069  fssres  6070  fcoi2  6079  fint  6084  fin  6085  f0  6086  fconst  6091  f1ssr  6107  fof  6115  dff1o2  6142  dff2  6371  dff3  6372  fmpt  6381  ffnfv  6388  ffvresb  6394  fpr  6421  idref  6499  dff1o6  6531  fliftf  6565  fun11iun  7126  ffoss  7127  1stcof  7196  2ndcof  7197  smores  7449  smores2  7451  iordsmo  7454  sbthlem9  8078  sucdom2  8156  inf3lem6  8530  alephsmo  8925  alephsing  9098  axdc3lem2  9273  smobeth  9408  fpwwe2lem11  9462  gch3  9498  gruiun  9621  gruima  9624  nqerf  9752  om2uzf1oi  12752  fclim  14284  invf  16428  funcres2b  16557  funcres2c  16561  hofcllem  16898  hofcl  16899  gsumval2  17280  resmhm2b  17361  frmdss2  17400  gsumval3a  18304  subgdmdprd  18433  srgfcl  18515  lsslindf  20169  indlcim  20179  cnrest2  21090  lmss  21102  conncn  21229  txflf  21810  cnextf  21870  clsnsg  21913  tgpconncomp  21916  psmetxrge0  22118  causs  23096  ellimc2  23641  perfdvf  23667  c1lip2  23761  dvne0  23774  plyeq0  23967  plyreres  24038  aannenlem1  24083  taylf  24115  ulmss  24151  mptelee  25775  ausgrusgrb  26060  ausgrumgri  26062  usgrexmplef  26151  subuhgr  26178  subupgr  26179  subumgr  26180  subusgr  26181  upgrres  26198  umgrres  26199  hhssnv  28121  pjfi  28563  maprnin  29506  measdivcstOLD  30287  sitgf  30409  eulerpartlemn  30443  reprinrn  30696  cvmlift2lem9a  31285  elno2  31807  elno3  31808  scutf  31919  icoreresf  33200  poimirlem30  33439  poimirlem31  33440  isbnd3  33583  dihf11lem  36555  ntrf  38421  clsf2  38424  gneispace3  38431  gneispacef2  38434  gneispacern  38436  k0004lem1  38445  dvsid  38530  stoweidlem27  40244  stoweidlem29  40246  stoweidlem31  40248  fourierdlem15  40339  mbfresmf  40948  ffnafv  41251  iccpartf  41367  resmgmhm2b  41800