Definition df-fn 6140

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6295, dffn3 6304, dffn4 6374, and dffn5 6503. (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 6132	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6131	. . 3 wff Fun 𝐴
5	1	cdm 5357	. . . 4 class dom 𝐴
6	5, 2	wceq 1601	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 386	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 198	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6167  fnsng  6188  fnprg  6195  fntpg  6196  fntp  6197  fncnv  6209  fneq1  6226  fneq2  6227  nffn  6234  fnfun  6235  fndm  6237  fnun  6245  fnco  6247  fnssresb  6251  fnres  6255  fnresi  6256  fn0  6259  mptfnf  6263  fnopabg  6265  sbcfng  6290  fdmrn  6316  fcoi1  6330  f00  6339  f1cnvcnv  6362  fores  6378  dff1o4  6401  foimacnv  6410  funfv  6527  fvimacnvALT  6601  respreima  6610  dff3  6638  fpr  6689  fnsnb  6701  fnprb  6746  fnex  6755  fliftf  6839  fnoprabg  7040  fun11iun  7407  f1oweALT  7431  curry1  7552  curry2  7555  tposfn2  7658  wfrlem13  7712  wfr1  7718  tfrlem10  7768  tfr1  7778  frfnom  7815  undifixp  8232  sbthlem9  8368  fodomr  8401  rankf  8956  cardf2  9104  axdc3lem2  9610  nqerf  10089  axaddf  10304  axmulf  10305  uzrdgfni  13081  hashkf  13443  shftfn  14226  imasaddfnlem  16585  imasvscafn  16594  fntopon  21147  cnextf  22289  ftc1cn  24254  grporn  27965  ffsrn  30087  measdivcstOLD  30893  bnj1422  31515  nofnbday  32402  elno2  32404  scutf  32516  fnsingle  32623  fnimage  32633  imageval  32634  dfrecs2  32654  dfrdg4  32655  ftc1cnnc  34118  fnresfnco  42119  funcoressn  42120  afvco2  42231