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

Definition df-fn 5441
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5578, dffn3 5584, dffn4 5643, and dffn5 5753. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-fn

Detailed syntax breakdown of Definition df-fn
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2wfn 5433 . 2
41wfun 5432 . . 3
51cdm 4862 . . . 4
65, 2wceq 1670 . . 3
74, 6wa 360 . 2
83, 7wb 178 1
Colors of variables: wff set class
This definition is referenced by:  funfn  5467  fnsng  5483  fnprg  5490  fntpg  5491  fntp  5492  fncnv  5500  fneq1  5517  fneq2  5518  nffn  5525  fnfun  5526  fndm  5528  fnun  5535  fnco  5537  fnssresb  5541  fnres  5545  fnresi  5546  fn0  5548  fnopabg  5552  sbcfng  5574  fcoi1  5602  f00  5610  f1cnvcnv  5631  fores  5646  dff1o4  5666  foimacnv  5675  funfv  5774  fvimacnvALT  5838  respreima  5848  dff3  5872  fpr  5905  fnsnb  5913  fnprb  5951  fnprOLD  5952  fnex  5959  fliftf  6018  fnoprabg  6203  fun11iun  6544  f1oweALT  6567  curry1  6670  curry2  6673  tposfn2  6733  tfrlem10  6810  tfr1  6820  frfnom  6854  undifixp  7262  sbthlem9  7390  fodomr  7423  rankf  7887  cardf2  7999  axdc3lem2  8502  nqerf  8978  axaddf  9191  axmulf  9192  uzrdgfni  11630  hashkf  11954  shftfn  12409  imasaddfnlem  14307  imasvscafn  14316  cnrest  18363  cnextf  19112  ftc1cn  20942  grporn  22821  fdmrn  25074  mptfnf  25106  ffsrn  25159  measdivcstOLD  25818  wfrlem13  26889  wfr1  26893  nofnbday  26946  elno2  26948  bdayfn  26973  fnsingle  27103  fnimage  27113  imageval  27114  dfrdg4  27134  tfrqfree  27135  ftc1cnnc  27646  fnresfnco  29211  funcoressn  29212  afvco2  29261  bnj145OLD  30564  bnj1422  30679
  Copyright terms: Public domain W3C validator