Definition df-fn 6530

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6699, dffn3 6710, dffn4 6790, and dffn5 6931. (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 6522	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6521	. . 3 wff Fun 𝐴
5	1	cdm 5647	. . . 4 class dom 𝐴
6	5, 2	wceq 1570	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 401	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 209	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is used by:  funfn  6558  fnsng  6580  fnprg  6587  fntpg  6588  fntp  6589  fncnv  6601  fneq1  6618  fneq2  6619  nffn  6626  fnfun  6627  fndm  6630  fnun  6641  fnssresb  6649  fnres  6654  idfn  6655  fn0  6658  mptfnf  6662  fnopabg  6664  sbcfng  6694  fdmrn  6729  fcoi1  6744  f00  6752  f1cnvcnv  6777  fores  6794  dff1o4  6821  foimacnv  6830  funfv  6960  fvimacnvALT  7044  respreima  7053  dff3  7088  fpr  7146  fnsnbOLD  7159  fnprb  7202  fnex  7211  fliftf  7311  fnoprabg  7531  fiun  7938  f1iun  7939  f1oweALT  7967  curry1  8098  curry2  8101  tposfn2  8243  frrlem11  8292  frrlem12  8293  fpr1  8299  tfrlem10  8373  tfr1  8383  frfnom  8421  undifixp  8940  sbthlem9  9092  fodomr  9125  fodomfir  9297  frr1  9741  rankf  9776  cardf2  9995  axdc3lem2  10500  nqerf  10986  axaddf  11201  axmulf  11202  uzrdgfni  14069  hashkf  14443  shftfn  15193  sgnfo  15219  imasaddfnlem  17661  imasvscafn  17670  nfchnd  18746  mgmn0plusgf  18788  degenmgmnfn  19097  fntopon  23203  cnextf  24346  ftc1cn  26324  nofnbday  27942  cutsf  28111  oniso  28590  noseqrdgfn  28625  bdayn0sf1o  28689  grporn  31056  ffsrn  33253  measdivcstALTV  34791  bnj1422  35401  satff  36096  fnsingle  36603  fnimage  36613  imageval  36614  dfrecs2  36636  dfrdg4  36637  bj-isrvec  38135  ftc1cnnc  38530  modelaxreplem1  45905  fnresfnco  48033  funcoressn  48034  afvco2  48168