Definition df-fn 6327

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6489, dffn3 6499, dffn4 6571, and dffn5 6699. (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 6319	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6318	. . 3 wff Fun 𝐴
5	1	cdm 5519	. . . 4 class dom 𝐴
6	5, 2	wceq 1538	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 399	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 209	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6354  fnsng  6376  fnprg  6383  fntpg  6384  fntp  6385  fncnv  6397  fneq1  6414  fneq2  6415  nffn  6422  fnfun  6423  fndm  6425  fnun  6434  fnco  6437  fnssresb  6441  fnres  6446  idfn  6447  fnresiOLD  6449  fn0  6451  mptfnf  6455  fnopabg  6457  sbcfng  6484  fdmrn  6512  fcoi1  6526  f00  6535  f1cnvcnv  6559  fores  6575  dff1o4  6598  foimacnv  6607  funfv  6725  fvimacnvALT  6804  respreima  6813  dff3  6843  fpr  6893  fnsnb  6905  fnprb  6948  fnex  6957  fliftf  7047  fnoprabg  7254  fiun  7626  f1iun  7627  f1oweALT  7655  curry1  7782  curry2  7785  tposfn2  7897  wfrlem13  7950  wfr1  7956  tfrlem10  8006  tfr1  8016  frfnom  8053  undifixp  8481  sbthlem9  8619  fodomr  8652  rankf  9207  cardf2  9356  axdc3lem2  9862  nqerf  10341  axaddf  10556  axmulf  10557  uzrdgfni  13321  hashkf  13688  shftfn  14424  imasaddfnlem  16793  imasvscafn  16802  fntopon  21529  cnextf  22671  ftc1cn  24646  grporn  28304  ffsrn  30491  measdivcstALTV  31594  bnj1422  32219  satff  32770  frrlem11  33246  frrlem12  33247  fpr1  33252  frr1  33257  nofnbday  33272  scutf  33386  fnsingle  33493  fnimage  33503  imageval  33504  dfrecs2  33524  dfrdg4  33525  ftc1cnnc  35129  fnresfnco  43633  funcoressn  43634  afvco2  43732