Definition df-fn 6418

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6583, dffn3 6594, dffn4 6675, and dffn5 6807. (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 6410	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6409	. . 3 wff Fun 𝐴
5	1	cdm 5579	. . . 4 class dom 𝐴
6	5, 2	wceq 1543	. . 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  6445  fnsng  6467  fnprg  6474  fntpg  6475  fntp  6476  fncnv  6488  fneq1  6505  fneq2  6506  nffn  6513  fnfun  6514  fndm  6517  fnun  6526  fncoOLD  6531  fnssresb  6535  fnres  6540  idfn  6541  fnresiOLD  6543  fn0  6545  mptfnf  6549  fnopabg  6551  sbcfng  6578  fdmrn  6613  fcoi1  6629  f00  6637  f1cnvcnv  6661  fores  6679  dff1o4  6705  foimacnv  6714  funfv  6834  fvimacnvALT  6913  respreima  6922  dff3  6955  fpr  7005  fnsnb  7017  fnprb  7063  fnex  7072  fliftf  7163  fnoprabg  7372  fiun  7756  f1iun  7757  f1oweALT  7785  curry1  7912  curry2  7915  tposfn2  8032  frrlem11  8079  frrlem12  8080  fpr1  8085  wfrlem13  8109  wfr1  8115  tfrlem10  8165  tfr1  8175  frfnom  8212  undifixp  8657  sbthlem9  8808  fodomr  8841  frr1  9423  rankf  9458  cardf2  9607  axdc3lem2  10113  nqerf  10592  axaddf  10807  axmulf  10808  uzrdgfni  13581  hashkf  13949  shftfn  14687  imasaddfnlem  17131  imasvscafn  17140  fntopon  21956  cnextf  23100  ftc1cn  25087  grporn  28759  ffsrn  30941  measdivcstALTV  32068  bnj1422  32692  satff  33247  nofnbday  33757  scutf  33908  fnsingle  34123  fnimage  34133  imageval  34134  dfrecs2  34154  dfrdg4  34155  bj-isrvec  35368  ftc1cnnc  35755  fnresfnco  44395  funcoressn  44396  afvco2  44528