Definition df-fn 5636

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5786, dffn3 5793, dffn4 5858, and dffn5 5975. (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 5628	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5627	. . 3 wff Fun 𝐴
5	1	cdm 4880	. . . 4 class dom 𝐴
6	5, 2	wceq 1468	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 378	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 191	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  5662  fnsng  5681  fnprg  5688  fntpg  5689  fntp  5690  fncnv  5702  fneq1  5719  fneq2  5720  nffn  5727  fnfun  5728  fndm  5730  fnun  5737  fnco  5739  fnssresb  5743  fnres  5747  fnresi  5748  fn0  5750  mptfnf  5754  fnopabg  5756  sbcfng  5781  fdmrn  5802  fcoi1  5815  f00  5824  f1cnvcnv  5846  fores  5861  dff1o4  5882  foimacnv  5891  funfv  5999  fvimacnvALT  6068  respreima  6076  dff3  6102  fpr  6140  fnsnb  6151  fnprb  6191  fnex  6200  fliftf  6279  fnoprabg  6472  fun11iun  6830  f1oweALT  6854  curry1  6967  curry2  6970  tposfn2  7072  wfrlem13  7125  wfr1  7131  tfrlem10  7182  tfr1  7192  frfnom  7229  undifixp  7641  sbthlem9  7774  fodomr  7807  rankf  8350  cardf2  8462  axdc3lem2  8966  nqerf  9440  axaddf  9654  axmulf  9655  uzrdgfni  12285  hashkf  12631  shftfn  13296  imasaddfnlem  15599  imasvscafn  15608  cnextf  21239  ftc1cn  23156  grporn  26103  ffsrn  28470  measdivcstOLD  29201  bnj145OLD  29688  bnj1422  29801  nofnbday  30690  elno2  30692  bdayfn  30719  fnsingle  30837  fnimage  30847  imageval  30848  dfrecs2  30868  dfrdg4  30869  bj-fntopon  31842  ftc1cnnc  32254  fnresfnco  39147  funcoressn  39148  afvco2  39198