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 1539	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 394	. 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  7155  fnsnb  7167  fnprb  7213  fnex  7222  fliftf  7316  fnoprabg  7535  fiun  7933  f1iun  7934  f1oweALT  7963  curry1  8094  curry2  8097  tposfn2  8237  frrlem11  8285  frrlem12  8286  fpr1  8292  wfrlem13OLD  8325  wfr1OLD  8331  tfrlem10  8391  tfr1  8401  frfnom  8439  undifixp  8932  sbthlem9  9095  fodomr  9132  frr1  9758  rankf  9793  cardf2  9942  axdc3lem2  10450  nqerf  10929  axaddf  11144  axmulf  11145  uzrdgfni  13929  hashkf  14298  shftfn  15026  imasaddfnlem  17480  imasvscafn  17489  fntopon  22648  cnextf  23792  ftc1cn  25794  nofnbday  27389  scutf  27548  grporn  30039  ffsrn  32219  measdivcstALTV  33519  bnj1422  34144  satff  34697  fnsingle  35193  fnimage  35203  imageval  35204  dfrecs2  35224  dfrdg4  35225  bj-isrvec  36480  ftc1cnnc  36865  fnresfnco  46051  funcoressn  46052  afvco2  46184