Definition df-f 6565

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 7119, dff3 7120, and dff4 7121. (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 6557	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6556	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5686	. . . 4 class ran 𝐹
7	6, 2	wss 3951	. . 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  6716  feq2  6717  feq3  6718  nff  6732  sbcfg  6734  ffn  6736  dffn2  6738  frn  6743  dffn3  6748  ffrnb  6750  fss  6752  fcof  6759  funssxp  6764  fdmrn  6767  fun  6770  fnfco  6773  fssres  6774  fcoi2  6783  fint  6787  fin  6788  f0  6789  fconst  6794  f1ssr  6810  fof  6820  dff1o2  6853  dff2  7119  dff3  7120  fmpt  7130  ffnfv  7139  ffvresb  7145  idref  7166  fpr  7174  dff1o6  7295  fliftf  7335  fiun  7967  f1iun  7968  ffoss  7970  1stcof  8044  2ndcof  8045  smores  8392  smores2  8394  iordsmo  8397  sbthlem9  9131  inf3lem6  9673  alephsmo  10142  alephsing  10316  axdc3lem2  10491  smobeth  10626  fpwwe2lem10  10680  gruiun  10839  gruima  10842  nqerf  10970  om2uzf1oi  13994  fclim  15589  invf  17812  funcres2b  17942  funcres2c  17948  hofcllem  18303  hofcl  18304  gsumval2  18699  resmgmhm2b  18726  resmhm2b  18835  frmdss2  18876  gsumval3a  19921  subgdmdprd  20054  srgfcl  20193  lsslindf  21850  indlcim  21860  cnrest2  23294  lmss  23306  conncn  23434  txflf  24014  cnextf  24074  clsnsg  24118  tgpconncomp  24121  psmetxrge0  24323  causs  25332  ellimc2  25912  perfdvf  25938  c1lip2  26037  dvne0  26050  plyeq0  26250  plyreres  26324  aannenlem1  26370  taylf  26402  ulmss  26440  elno2  27699  elno3  27700  scutf  27857  madef  27895  mptelee  28910  ausgrusgrb  29182  ausgrumgri  29184  usgrexmplef  29276  subuhgr  29303  subupgr  29304  subumgr  29305  subusgr  29306  upgrres  29323  umgrres  29324  hhssnv  31283  pjfi  31723  maprnin  32742  cycpmconjslem1  33174  measdivcstALTV  34226  sitgf  34349  eulerpartlemn  34383  reprinrn  34633  cvmlift2lem9a  35308  satff  35415  icoreresf  37353  poimirlem30  37657  poimirlem31  37658  isbnd3  37791  dihf11lem  41268  ofoafg  43367  ofoaid1  43371  ofoaid2  43372  naddcnff  43375  ntrf  44136  clsf2  44139  gneispace3  44146  gneispacef2  44149  k0004lem1  44160  dvsid  44350  stoweidlem27  46042  stoweidlem29  46044  stoweidlem31  46046  fourierdlem15  46137  mbfresmf  46754  ffnafv  47183  fcdmvafv2v  47248  iccpartf  47418