MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fn Structured version   Visualization version   GIF version

Definition df-fn 6352
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6510, dffn3 6519, dffn4 6590, and dffn5 6718. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-fn (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

Detailed syntax breakdown of Definition df-fn
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wfn 6344 . 2 wff 𝐴 Fn 𝐵
41wfun 6343 . . 3 wff Fun 𝐴
51cdm 5549 . . . 4 class dom 𝐴
65, 2wceq 1528 . . 3 wff dom 𝐴 = 𝐵
74, 6wa 396 . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
83, 7wb 207 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  funfn  6379  fnsng  6400  fnprg  6407  fntpg  6408  fntp  6409  fncnv  6421  fneq1  6438  fneq2  6439  nffn  6446  fnfun  6447  fndm  6449  fnun  6457  fnco  6459  fnssresb  6463  fnres  6468  idfn  6469  fnresiOLD  6471  fn0  6473  mptfnf  6477  fnopabg  6479  sbcfng  6505  fdmrn  6532  fcoi1  6546  f00  6555  f1cnvcnv  6578  fores  6594  dff1o4  6617  foimacnv  6626  funfv  6744  fvimacnvALT  6820  respreima  6829  dff3  6859  fpr  6909  fnsnb  6921  fnprb  6963  fnex  6972  fliftf  7057  fnoprabg  7264  fiunw  7632  f1iunw  7633  fiun  7635  f1iun  7636  f1oweALT  7664  curry1  7790  curry2  7793  tposfn2  7905  wfrlem13  7958  wfr1  7964  tfrlem10  8014  tfr1  8024  frfnom  8061  undifixp  8487  sbthlem9  8624  fodomr  8657  rankf  9212  cardf2  9361  axdc3lem2  9862  nqerf  10341  axaddf  10556  axmulf  10557  uzrdgfni  13316  hashkf  13682  shftfn  14422  imasaddfnlem  16791  imasvscafn  16800  fntopon  21462  cnextf  22604  ftc1cn  24569  grporn  28226  ffsrn  30392  measdivcstALTV  31384  bnj1422  32009  satff  32555  frrlem11  33031  frrlem12  33032  fpr1  33037  frr1  33042  nofnbday  33057  scutf  33171  fnsingle  33278  fnimage  33288  imageval  33289  dfrecs2  33309  dfrdg4  33310  ftc1cnnc  34848  fnresfnco  43157  funcoressn  43158  afvco2  43256
  Copyright terms: Public domain W3C validator