Definition df-fn 6564

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6738, dffn3 6748, dffn4 6826, and dffn5 6967. (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 6556	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6555	. . 3 wff Fun 𝐴
5	1	cdm 5685	. . . 4 class dom 𝐴
6	5, 2	wceq 1540	. . 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  6596  fnsng  6618  fnprg  6625  fntpg  6626  fntp  6627  fncnv  6639  fneq1  6659  fneq2  6660  nffn  6667  fnfun  6668  fndm  6671  fnun  6682  fnssresb  6690  fnres  6695  idfn  6696  fn0  6699  mptfnf  6703  fnopabg  6705  sbcfng  6733  fdmrn  6767  fcoi1  6782  f00  6790  f1cnvcnv  6813  fores  6830  dff1o4  6856  foimacnv  6865  funfv  6996  fvimacnvALT  7077  respreima  7086  dff3  7120  fpr  7174  fnsnb  7186  fnprb  7228  fnex  7237  fliftf  7335  fnoprabg  7556  fiun  7967  f1iun  7968  f1oweALT  7997  curry1  8129  curry2  8132  tposfn2  8273  frrlem11  8321  frrlem12  8322  fpr1  8328  wfrlem13OLD  8361  wfr1OLD  8367  tfrlem10  8427  tfr1  8437  frfnom  8475  undifixp  8974  sbthlem9  9131  fodomr  9168  fodomfir  9368  frr1  9799  rankf  9834  cardf2  9983  axdc3lem2  10491  nqerf  10970  axaddf  11185  axmulf  11186  uzrdgfni  13999  hashkf  14371  shftfn  15112  imasaddfnlem  17573  imasvscafn  17582  fntopon  22930  cnextf  24074  ftc1cn  26084  nofnbday  27697  scutf  27857  noseqrdgfn  28312  grporn  30540  ffsrn  32740  measdivcstALTV  34226  bnj1422  34851  satff  35415  fnsingle  35920  fnimage  35930  imageval  35931  dfrecs2  35951  dfrdg4  35952  bj-isrvec  37295  ftc1cnnc  37699  modelaxreplem1  44995  fnresfnco  47053  funcoressn  47054  afvco2  47188