Definition df-fn 6533

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6707, dffn3 6717, dffn4 6795, and dffn5 6936. (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 6525	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6524	. . 3 wff Fun 𝐴
5	1	cdm 5654	. . . 4 class dom 𝐴
6	5, 2	wceq 1540	. . 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  6565  fnsng  6587  fnprg  6594  fntpg  6595  fntp  6596  fncnv  6608  fneq1  6628  fneq2  6629  nffn  6636  fnfun  6637  fndm  6640  fnun  6651  fnssresb  6659  fnres  6664  idfn  6665  fn0  6668  mptfnf  6672  fnopabg  6674  sbcfng  6702  fdmrn  6736  fcoi1  6751  f00  6759  f1cnvcnv  6782  fores  6799  dff1o4  6825  foimacnv  6834  funfv  6965  fvimacnvALT  7046  respreima  7055  dff3  7089  fpr  7143  fnsnbOLD  7157  fnprb  7199  fnex  7208  fliftf  7307  fnoprabg  7528  fiun  7939  f1iun  7940  f1oweALT  7969  curry1  8101  curry2  8104  tposfn2  8245  frrlem11  8293  frrlem12  8294  fpr1  8300  wfrlem13OLD  8333  wfr1OLD  8339  tfrlem10  8399  tfr1  8409  frfnom  8447  undifixp  8946  sbthlem9  9103  fodomr  9140  fodomfir  9338  frr1  9771  rankf  9806  cardf2  9955  axdc3lem2  10463  nqerf  10942  axaddf  11157  axmulf  11158  uzrdgfni  13974  hashkf  14348  shftfn  15090  imasaddfnlem  17540  imasvscafn  17549  fntopon  22860  cnextf  24002  ftc1cn  26000  nofnbday  27614  scutf  27774  noseqrdgfn  28229  grporn  30448  ffsrn  32652  measdivcstALTV  34202  bnj1422  34814  satff  35378  fnsingle  35883  fnimage  35893  imageval  35894  dfrecs2  35914  dfrdg4  35915  bj-isrvec  37258  ftc1cnnc  37662  modelaxreplem1  44951  fnresfnco  47018  funcoressn  47019  afvco2  47153