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 5661	. . . 4 class dom 𝐴
6	5, 2	wceq 1568	. . 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 referenced 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  7533  fiun  7939  f1iun  7940  f1oweALT  7968  curry1  8098  curry2  8101  tposfn2  8243  frrlem11  8292  frrlem12  8293  fpr1  8299  tfrlem10  8373  tfr1  8383  frfnom  8421  undifixp  8931  sbthlem9  9082  fodomr  9115  fodomfir  9286  frr1  9730  rankf  9765  cardf2  9928  axdc3lem2  10434  nqerf  10914  axaddf  11129  axmulf  11130  uzrdgfni  13993  hashkf  14367  shftfn  15109  sgnfo  15135  imasaddfnlem  17581  imasvscafn  17590  nfchnd  18666  fntopon  23060  cnextf  24202  ftc1cn  26181  nofnbday  27792  cutsf  27961  oniso  28440  noseqrdgfn  28475  bdayn0sf1o  28539  grporn  30839  ffsrn  33039  measdivcstALTV  34581  bnj1422  35191  satff  35856  fnsingle  36363  fnimage  36373  imageval  36374  dfrecs2  36396  dfrdg4  36397  bj-isrvec  37882  ftc1cnnc  38287  modelaxreplem1  45635  fnresfnco  47723  funcoressn  47724  afvco2  47858