Definition df-fn 6540

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6708, dffn3 6719, dffn4 6799, and dffn5 6940. (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 6532	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6531	. . 3 wff Fun 𝐴
5	1	cdm 5659	. . . 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  6567  fnsng  6589  fnprg  6596  fntpg  6597  fntp  6598  fncnv  6610  fneq1  6627  fneq2  6628  nffn  6635  fnfun  6636  fndm  6639  fnun  6650  fnssresb  6658  fnres  6663  idfn  6664  fn0  6667  mptfnf  6671  fnopabg  6673  sbcfng  6703  fdmrn  6738  fcoi1  6753  f00  6761  f1cnvcnv  6786  fores  6803  dff1o4  6830  foimacnv  6839  funfv  6969  fvimacnvALT  7053  respreima  7062  dff3  7096  fpr  7154  fnsnbOLD  7167  fnprb  7210  fnex  7219  fliftf  7319  fnoprabg  7539  fiun  7943  f1iun  7944  f1oweALT  7972  curry1  8104  curry2  8107  tposfn2  8249  frrlem11  8298  frrlem12  8299  fpr1  8305  tfrlem10  8379  tfr1  8389  frfnom  8427  undifixp  8944  sbthlem9  9096  fodomr  9129  fodomfir  9300  frr1  9744  rankf  9779  cardf2  9951  axdc3lem2  10456  nqerf  10940  axaddf  11155  axmulf  11156  uzrdgfni  14022  hashkf  14396  shftfn  15146  sgnfo  15172  imasaddfnlem  17616  imasvscafn  17625  nfchnd  18701  mgmn0plusgf  18743  degenmgmnfn  19048  fntopon  23148  cnextf  24291  ftc1cn  26270  nofnbday  27884  cutsf  28053  oniso  28532  noseqrdgfn  28567  bdayn0sf1o  28631  grporn  30986  ffsrn  33184  measdivcstALTV  34721  bnj1422  35331  satff  35974  fnsingle  36481  fnimage  36491  imageval  36492  dfrecs2  36514  dfrdg4  36515  bj-isrvec  38031  ftc1cnnc  38426  modelaxreplem1  45786  fnresfnco  47914  funcoressn  47915  afvco2  48049