Definition df-fn 6576

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6749, dffn3 6759, dffn4 6840, and dffn5 6980. (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 6568	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6567	. . 3 wff Fun 𝐴
5	1	cdm 5700	. . . 4 class dom 𝐴
6	5, 2	wceq 1537	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 395	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 206	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6608  fnsng  6630  fnprg  6637  fntpg  6638  fntp  6639  fncnv  6651  fneq1  6670  fneq2  6671  nffn  6678  fnfun  6679  fndm  6682  fnun  6693  fncoOLD  6698  fnssresb  6702  fnres  6707  idfn  6708  fn0  6711  mptfnf  6715  fnopabg  6717  sbcfng  6744  fdmrn  6779  fcoi1  6795  f00  6803  f1cnvcnv  6826  fores  6844  dff1o4  6870  foimacnv  6879  funfv  7009  fvimacnvALT  7090  respreima  7099  dff3  7134  fpr  7188  fnsnb  7200  fnprb  7245  fnex  7254  fliftf  7351  fnoprabg  7573  fiun  7983  f1iun  7984  f1oweALT  8013  curry1  8145  curry2  8148  tposfn2  8289  frrlem11  8337  frrlem12  8338  fpr1  8344  wfrlem13OLD  8377  wfr1OLD  8383  tfrlem10  8443  tfr1  8453  frfnom  8491  undifixp  8992  sbthlem9  9157  fodomr  9194  fodomfir  9396  frr1  9828  rankf  9863  cardf2  10012  axdc3lem2  10520  nqerf  10999  axaddf  11214  axmulf  11215  uzrdgfni  14009  hashkf  14381  shftfn  15122  imasaddfnlem  17588  imasvscafn  17597  fntopon  22951  cnextf  24095  ftc1cn  26104  nofnbday  27715  scutf  27875  noseqrdgfn  28330  grporn  30553  ffsrn  32743  measdivcstALTV  34189  bnj1422  34813  satff  35378  fnsingle  35883  fnimage  35893  imageval  35894  dfrecs2  35914  dfrdg4  35915  bj-isrvec  37260  ftc1cnnc  37652  fnresfnco  46956  funcoressn  46957  afvco2  47091