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 5697
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5850, dffn3 5857, dffn4 5923, and dffn5 6040. (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 5689 . 2 wff 𝐴 Fn 𝐵
41wfun 5688 . . 3 wff Fun 𝐴
51cdm 4932 . . . 4 class dom 𝐴
65, 2wceq 1474 . . 3 wff dom 𝐴 = 𝐵
74, 6wa 382 . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
83, 7wb 194 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  funfn  5723  fnsng  5742  fnprg  5751  fntpg  5752  fntp  5753  fncnv  5766  fneq1  5783  fneq2  5784  nffn  5791  fnfun  5792  fndm  5794  fnun  5801  fnco  5803  fnssresb  5807  fnres  5811  fnresi  5812  fn0  5814  mptfnf  5818  fnopabg  5820  sbcfng  5845  fdmrn  5867  fcoi1  5880  f00  5889  f1cnvcnv  5911  fores  5926  dff1o4  5947  foimacnv  5956  funfv  6064  fvimacnvALT  6133  respreima  6141  dff3  6169  fpr  6208  fnsnb  6219  fnprb  6259  fnex  6268  fliftf  6347  fnoprabg  6541  fun11iun  6899  f1oweALT  6923  curry1  7036  curry2  7039  tposfn2  7141  wfrlem13  7194  wfr1  7200  tfrlem10  7250  tfr1  7260  frfnom  7297  undifixp  7710  sbthlem9  7843  fodomr  7876  rankf  8420  cardf2  8532  axdc3lem2  9036  nqerf  9511  axaddf  9725  axmulf  9726  uzrdgfni  12491  hashkf  12853  shftfn  13524  imasaddfnlem  15907  imasvscafn  15916  cnextf  21587  ftc1cn  23489  grporn  26501  ffsrn  28684  measdivcstOLD  29414  bnj145OLD  29898  bnj1422  30011  nofnbday  30888  elno2  30890  bdayfn  30917  fnsingle  31035  fnimage  31045  imageval  31046  dfrecs2  31066  dfrdg4  31067  bj-fntopon  32078  ftc1cnnc  32548  fnresfnco  39766  funcoressn  39767  afvco2  39817
  Copyright terms: Public domain W3C validator