Definition df-fn 6491

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6660, dffn3 6670, dffn4 6748, and dffn5 6888. (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 6483	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6482	. . 3 wff Fun 𝐴
5	1	cdm 5620	. . . 4 class dom 𝐴
6	5, 2	wceq 1548	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 397	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 208	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6518  fnsng  6540  fnprg  6547  fntpg  6548  fntp  6549  fncnv  6561  fneq1  6579  fneq2  6580  nffn  6587  fnfun  6588  fndm  6591  fnun  6602  fnssresb  6610  fnres  6615  idfn  6616  fn0  6619  mptfnf  6623  fnopabg  6625  sbcfng  6655  fdmrn  6689  fcoi1  6704  f00  6712  f1cnvcnv  6735  fores  6752  dff1o4  6778  foimacnv  6787  funfv  6917  fvimacnvALT  7001  respreima  7010  dff3  7044  fpr  7100  fnsnbOLD  7113  fnprb  7155  fnex  7164  fliftf  7262  fnoprabg  7482  fiun  7887  f1iun  7888  f1oweALT  7916  curry1  8045  curry2  8048  tposfn2  8190  frrlem11  8239  frrlem12  8240  fpr1  8246  tfrlem10  8320  tfr1  8330  frfnom  8368  undifixp  8876  sbthlem9  9027  fodomr  9060  fodomfir  9232  frr1  9678  rankf  9713  cardf2  9862  axdc3lem2  10369  nqerf  10849  axaddf  11064  axmulf  11065  uzrdgfni  13915  hashkf  14289  shftfn  15030  imasaddfnlem  17487  imasvscafn  17496  nfchnd  18572  fntopon  22910  cnextf  24052  ftc1cn  26031  nofnbday  27636  cutsf  27804  oniso  28283  noseqrdgfn  28318  bdayn0sf1o  28382  grporn  30612  ffsrn  32822  measdivcstALTV  34419  bnj1422  35032  satff  35651  fnsingle  36158  fnimage  36168  imageval  36169  dfrecs2  36191  dfrdg4  36192  bj-isrvec  37667  ftc1cnnc  38072  modelaxreplem1  45435  fnresfnco  47516  funcoressn  47517  afvco2  47651