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 5807
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5960, dffn3 5967, dffn4 6034, and dffn5 6151. (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 5799 . 2 wff 𝐴 Fn 𝐵
41wfun 5798 . . 3 wff Fun 𝐴
51cdm 5038 . . . 4 class dom 𝐴
65, 2wceq 1475 . . 3 wff dom 𝐴 = 𝐵
74, 6wa 383 . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
83, 7wb 195 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  funfn  5833  fnsng  5852  fnprg  5861  fntpg  5862  fntp  5863  fncnv  5876  fneq1  5893  fneq2  5894  nffn  5901  fnfun  5902  fndm  5904  fnun  5911  fnco  5913  fnssresb  5917  fnres  5921  fnresi  5922  fn0  5924  mptfnf  5928  fnopabg  5930  sbcfng  5955  fdmrn  5977  fcoi1  5991  f00  6000  f1cnvcnv  6022  fores  6037  dff1o4  6058  foimacnv  6067  funfv  6175  fvimacnvALT  6244  respreima  6252  dff3  6280  fpr  6326  fnsnb  6337  fnprb  6377  fnex  6386  fliftf  6465  fnoprabg  6659  fun11iun  7019  f1oweALT  7043  curry1  7156  curry2  7159  tposfn2  7261  wfrlem13  7314  wfr1  7320  tfrlem10  7370  tfr1  7380  frfnom  7417  undifixp  7830  sbthlem9  7963  fodomr  7996  rankf  8540  cardf2  8652  axdc3lem2  9156  nqerf  9631  axaddf  9845  axmulf  9846  uzrdgfni  12619  hashkf  12981  shftfn  13661  imasaddfnlem  16011  imasvscafn  16020  cnextf  21680  ftc1cn  23610  grporn  26759  ffsrn  28892  measdivcstOLD  29614  bnj145OLD  30049  bnj1422  30162  nofnbday  31049  elno2  31051  bdayfn  31078  fnsingle  31196  fnimage  31206  imageval  31207  dfrecs2  31227  dfrdg4  31228  bj-fntopon  32243  ftc1cnnc  32654  fnresfnco  39855  funcoressn  39856  afvco2  39905
  Copyright terms: Public domain W3C validator