Definition df-f 6534

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 7088, dff3 7089, and dff4 7090. (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 6526	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6525	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5655	. . . 4 class ran 𝐹
7	6, 2	wss 3926	. . 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  6685  feq2  6686  feq3  6687  nff  6701  sbcfg  6703  ffn  6705  dffn2  6707  frn  6712  dffn3  6717  ffrnb  6719  fss  6721  fcof  6728  funssxp  6733  fdmrn  6736  fun  6739  fnfco  6742  fssres  6743  fcoi2  6752  fint  6756  fin  6757  f0  6758  fconst  6763  f1ssr  6779  fof  6789  dff1o2  6822  dff2  7088  dff3  7089  fmpt  7099  ffnfv  7108  ffvresb  7114  idref  7135  fpr  7143  dff1o6  7267  fliftf  7307  fiun  7939  f1iun  7940  ffoss  7942  1stcof  8016  2ndcof  8017  smores  8364  smores2  8366  iordsmo  8369  sbthlem9  9103  inf3lem6  9645  alephsmo  10114  alephsing  10288  axdc3lem2  10463  smobeth  10598  fpwwe2lem10  10652  gruiun  10811  gruima  10814  nqerf  10942  om2uzf1oi  13969  fclim  15567  invf  17779  funcres2b  17908  funcres2c  17914  hofcllem  18268  hofcl  18269  gsumval2  18662  resmgmhm2b  18689  resmhm2b  18798  frmdss2  18839  gsumval3a  19882  subgdmdprd  20015  srgfcl  20154  lsslindf  21788  indlcim  21798  cnrest2  23222  lmss  23234  conncn  23362  txflf  23942  cnextf  24002  clsnsg  24046  tgpconncomp  24049  psmetxrge0  24250  causs  25248  ellimc2  25828  perfdvf  25854  c1lip2  25953  dvne0  25966  plyeq0  26166  plyreres  26240  aannenlem1  26286  taylf  26318  ulmss  26356  elno2  27616  elno3  27617  scutf  27774  madef  27812  mptelee  28820  ausgrusgrb  29090  ausgrumgri  29092  usgrexmplef  29184  subuhgr  29211  subupgr  29212  subumgr  29213  subusgr  29214  upgrres  29231  umgrres  29232  hhssnv  31191  pjfi  31631  maprnin  32654  cycpmconjslem1  33111  measdivcstALTV  34202  sitgf  34325  eulerpartlemn  34359  reprinrn  34596  cvmlift2lem9a  35271  satff  35378  icoreresf  37316  poimirlem30  37620  poimirlem31  37621  isbnd3  37754  dihf11lem  41231  ofoafg  43325  ofoaid1  43329  ofoaid2  43330  naddcnff  43333  ntrf  44094  clsf2  44097  gneispace3  44104  gneispacef2  44107  k0004lem1  44118  dvsid  44303  stoweidlem27  46004  stoweidlem29  46006  stoweidlem31  46008  fourierdlem15  46099  mbfresmf  46716  ffnafv  47148  fcdmvafv2v  47213  iccpartf  47393  slotresfo  48821