Definition df-fn 6505

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6674, dffn3 6684, dffn4 6762, and dffn5 6902. (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 6497	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6496	. . 3 wff Fun 𝐴
5	1	cdm 5634	. . . 4 class dom 𝐴
6	5, 2	wceq 1542	. . 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  6532  fnsng  6554  fnprg  6561  fntpg  6562  fntp  6563  fncnv  6575  fneq1  6593  fneq2  6594  nffn  6601  fnfun  6602  fndm  6605  fnun  6616  fnssresb  6624  fnres  6629  idfn  6630  fn0  6633  mptfnf  6637  fnopabg  6639  sbcfng  6669  fdmrn  6703  fcoi1  6718  f00  6726  f1cnvcnv  6749  fores  6766  dff1o4  6792  foimacnv  6801  funfv  6931  fvimacnvALT  7013  respreima  7022  dff3  7056  fpr  7111  fnsnbOLD  7124  fnprb  7166  fnex  7175  fliftf  7273  fnoprabg  7493  fiun  7899  f1iun  7900  f1oweALT  7928  curry1  8058  curry2  8061  tposfn2  8202  frrlem11  8250  frrlem12  8251  fpr1  8257  tfrlem10  8330  tfr1  8340  frfnom  8378  undifixp  8886  sbthlem9  9037  fodomr  9070  fodomfir  9242  frr1  9685  rankf  9720  cardf2  9869  axdc3lem2  10375  nqerf  10855  axaddf  11070  axmulf  11071  uzrdgfni  13895  hashkf  14269  shftfn  15010  imasaddfnlem  17463  imasvscafn  17472  nfchnd  18548  fntopon  22885  cnextf  24027  ftc1cn  26023  nofnbday  27637  cutsf  27805  oniso  28284  noseqrdgfn  28319  bdayn0sf1o  28383  grporn  30615  ffsrn  32824  measdivcstALTV  34409  bnj1422  35019  satff  35632  fnsingle  36139  fnimage  36149  imageval  36150  dfrecs2  36172  dfrdg4  36173  bj-isrvec  37576  ftc1cnnc  37972  modelaxreplem1  45363  fnresfnco  47430  funcoressn  47431  afvco2  47565