Definition df-fn 6490

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6659, dffn3 6669, dffn4 6747, and dffn5 6887. (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 6482	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6481	. . 3 wff Fun 𝐴
5	1	cdm 5620	. . . 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  6517  fnsng  6539  fnprg  6546  fntpg  6547  fntp  6548  fncnv  6560  fneq1  6578  fneq2  6579  nffn  6586  fnfun  6587  fndm  6590  fnun  6601  fnssresb  6609  fnres  6614  idfn  6615  fn0  6618  mptfnf  6622  fnopabg  6624  sbcfng  6654  fdmrn  6688  fcoi1  6703  f00  6711  f1cnvcnv  6734  fores  6751  dff1o4  6777  foimacnv  6786  funfv  6916  fvimacnvALT  6998  respreima  7007  dff3  7041  fpr  7097  fnsnbOLD  7110  fnprb  7152  fnex  7161  fliftf  7259  fnoprabg  7479  fiun  7885  f1iun  7886  f1oweALT  7914  curry1  8043  curry2  8046  tposfn2  8187  frrlem11  8235  frrlem12  8236  fpr1  8242  tfrlem10  8315  tfr1  8325  frfnom  8363  undifixp  8871  sbthlem9  9022  fodomr  9055  fodomfir  9227  frr1  9672  rankf  9707  cardf2  9856  axdc3lem2  10362  nqerf  10842  axaddf  11057  axmulf  11058  uzrdgfni  13909  hashkf  14283  shftfn  15024  imasaddfnlem  17481  imasvscafn  17490  nfchnd  18566  fntopon  22877  cnextf  24019  ftc1cn  25998  nofnbday  27604  cutsf  27772  oniso  28251  noseqrdgfn  28286  bdayn0sf1o  28350  grporn  30580  ffsrn  32789  measdivcstALTV  34357  bnj1422  34967  satff  35580  fnsingle  36087  fnimage  36097  imageval  36098  dfrecs2  36120  dfrdg4  36121  bj-isrvec  37596  ftc1cnnc  38001  modelaxreplem1  45393  fnresfnco  47477  funcoressn  47478  afvco2  47612