Definition df-fn 6539

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6707, dffn3 6718, dffn4 6798, and dffn5 6939. (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 6531	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6530	. . 3 wff Fun 𝐴
5	1	cdm 5660	. . . 4 class dom 𝐴
6	5, 2	wceq 1569	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 400	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 209	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is used by:  funfn  6566  fnsng  6588  fnprg  6595  fntpg  6596  fntp  6597  fncnv  6609  fneq1  6626  fneq2  6627  nffn  6634  fnfun  6635  fndm  6638  fnun  6649  fnssresb  6657  fnres  6662  idfn  6663  fn0  6666  mptfnf  6670  fnopabg  6672  sbcfng  6702  fdmrn  6737  fcoi1  6752  f00  6760  f1cnvcnv  6785  fores  6802  dff1o4  6829  foimacnv  6838  funfv  6968  fvimacnvALT  7052  respreima  7061  dff3  7095  fpr  7151  fnsnbOLD  7164  fnprb  7206  fnex  7215  fliftf  7313  fnoprabg  7535  fiun  7938  f1iun  7939  f1oweALT  7967  curry1  8097  curry2  8100  tposfn2  8242  frrlem11  8291  frrlem12  8292  fpr1  8298  tfrlem10  8372  tfr1  8382  frfnom  8420  undifixp  8930  sbthlem9  9081  fodomr  9114  fodomfir  9285  frr1  9729  rankf  9764  cardf2  9936  axdc3lem2  10441  nqerf  10921  axaddf  11136  axmulf  11137  uzrdgfni  14001  hashkf  14375  shftfn  15117  sgnfo  15143  imasaddfnlem  17588  imasvscafn  17597  nfchnd  18673  fntopon  23092  cnextf  24234  ftc1cn  26213  nofnbday  27827  cutsf  27996  oniso  28475  noseqrdgfn  28510  bdayn0sf1o  28574  grporn  30884  ffsrn  33084  measdivcstALTV  34624  bnj1422  35234  satff  35910  fnsingle  36417  fnimage  36427  imageval  36428  dfrecs2  36450  dfrdg4  36451  bj-isrvec  37966  ftc1cnnc  38371  modelaxreplem1  45715  fnresfnco  47806  funcoressn  47807  afvco2  47941