Definition df-fn 6358

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6516, dffn3 6525, dffn4 6596, and dffn5 6724. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-fn	⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

Detailed syntax breakdown of Definition df-fn

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	wfn 6350	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6349	. . 3 wff Fun 𝐴
5	1	cdm 5555	. . . 4 class dom 𝐴
6	5, 2	wceq 1537	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 398	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 208	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6385  fnsng  6406  fnprg  6413  fntpg  6414  fntp  6415  fncnv  6427  fneq1  6444  fneq2  6445  nffn  6452  fnfun  6453  fndm  6455  fnun  6463  fnco  6465  fnssresb  6469  fnres  6474  idfn  6475  fnresiOLD  6477  fn0  6479  mptfnf  6483  fnopabg  6485  sbcfng  6511  fdmrn  6538  fcoi1  6552  f00  6561  f1cnvcnv  6584  fores  6600  dff1o4  6623  foimacnv  6632  funfv  6750  fvimacnvALT  6827  respreima  6836  dff3  6866  fpr  6916  fnsnb  6928  fnprb  6971  fnex  6980  fliftf  7068  fnoprabg  7275  fiun  7644  f1iun  7645  f1oweALT  7673  curry1  7799  curry2  7802  tposfn2  7914  wfrlem13  7967  wfr1  7973  tfrlem10  8023  tfr1  8033  frfnom  8070  undifixp  8498  sbthlem9  8635  fodomr  8668  rankf  9223  cardf2  9372  axdc3lem2  9873  nqerf  10352  axaddf  10567  axmulf  10568  uzrdgfni  13327  hashkf  13693  shftfn  14432  imasaddfnlem  16801  imasvscafn  16810  fntopon  21532  cnextf  22674  ftc1cn  24640  grporn  28298  ffsrn  30465  measdivcstALTV  31484  bnj1422  32109  satff  32657  frrlem11  33133  frrlem12  33134  fpr1  33139  frr1  33144  nofnbday  33159  scutf  33273  fnsingle  33380  fnimage  33390  imageval  33391  dfrecs2  33411  dfrdg4  33412  ftc1cnnc  34981  fnresfnco  43296  funcoressn  43297  afvco2  43395