Definition df-fn 6547

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6720, dffn3 6731, dffn4 6812, and dffn5 6951. (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 6539	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6538	. . 3 wff Fun 𝐴
5	1	cdm 5677	. . . 4 class dom 𝐴
6	5, 2	wceq 1542	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 397	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 205	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6579  fnsng  6601  fnprg  6608  fntpg  6609  fntp  6610  fncnv  6622  fneq1  6641  fneq2  6642  nffn  6649  fnfun  6650  fndm  6653  fnun  6664  fncoOLD  6669  fnssresb  6673  fnres  6678  idfn  6679  fn0  6682  mptfnf  6686  fnopabg  6688  sbcfng  6715  fdmrn  6750  fcoi1  6766  f00  6774  f1cnvcnv  6798  fores  6816  dff1o4  6842  foimacnv  6851  funfv  6979  fvimacnvALT  7059  respreima  7068  dff3  7102  fpr  7152  fnsnb  7164  fnprb  7210  fnex  7219  fliftf  7312  fnoprabg  7531  fiun  7929  f1iun  7930  f1oweALT  7959  curry1  8090  curry2  8093  tposfn2  8233  frrlem11  8281  frrlem12  8282  fpr1  8288  wfrlem13OLD  8321  wfr1OLD  8327  tfrlem10  8387  tfr1  8397  frfnom  8435  undifixp  8928  sbthlem9  9091  fodomr  9128  frr1  9754  rankf  9789  cardf2  9938  axdc3lem2  10446  nqerf  10925  axaddf  11140  axmulf  11141  uzrdgfni  13923  hashkf  14292  shftfn  15020  imasaddfnlem  17474  imasvscafn  17483  fntopon  22426  cnextf  23570  ftc1cn  25560  nofnbday  27155  scutf  27313  grporn  29774  ffsrn  31954  measdivcstALTV  33223  bnj1422  33848  satff  34401  fnsingle  34891  fnimage  34901  imageval  34902  dfrecs2  34922  dfrdg4  34923  bj-isrvec  36175  ftc1cnnc  36560  fnresfnco  45751  funcoressn  45752  afvco2  45884