Definition df-fn 6526

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6695, dffn3 6706, dffn4 6786, and dffn5 6927. (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 6518	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6517	. . 3 wff Fun 𝐴
5	1	cdm 5649	. . . 4 class dom 𝐴
6	5, 2	wceq 1562	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 399	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 208	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6553  fnsng  6575  fnprg  6582  fntpg  6583  fntp  6584  fncnv  6596  fneq1  6614  fneq2  6615  nffn  6622  fnfun  6623  fndm  6626  fnun  6637  fnssresb  6645  fnres  6650  idfn  6651  fn0  6654  mptfnf  6658  fnopabg  6660  sbcfng  6690  fdmrn  6725  fcoi1  6740  f00  6748  f1cnvcnv  6773  fores  6790  dff1o4  6817  foimacnv  6826  funfv  6956  fvimacnvALT  7040  respreima  7049  dff3  7083  fpr  7139  fnsnbOLD  7152  fnprb  7194  fnex  7203  fliftf  7301  fnoprabg  7521  fiun  7926  f1iun  7927  f1oweALT  7955  curry1  8085  curry2  8088  tposfn2  8230  frrlem11  8279  frrlem12  8280  fpr1  8286  tfrlem10  8360  tfr1  8370  frfnom  8408  undifixp  8918  sbthlem9  9069  fodomr  9102  fodomfir  9274  frr1  9719  rankf  9754  cardf2  9903  axdc3lem2  10410  nqerf  10890  axaddf  11105  axmulf  11106  uzrdgfni  13973  hashkf  14347  shftfn  15088  sgnfo  15114  imasaddfnlem  17560  imasvscafn  17569  nfchnd  18645  fntopon  22986  cnextf  24128  ftc1cn  26107  nofnbday  27718  cutsf  27887  oniso  28366  noseqrdgfn  28401  bdayn0sf1o  28465  grporn  30726  ffsrn  32932  measdivcstALTV  34524  bnj1422  35134  satff  35765  fnsingle  36272  fnimage  36282  imageval  36283  dfrecs2  36305  dfrdg4  36306  bj-isrvec  37791  ftc1cnnc  38196  modelaxreplem1  45559  fnresfnco  47640  funcoressn  47641  afvco2  47775