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 5879
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6034, dffn3 6041, dffn4 6108, and dffn5 6228. (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 5871 . 2 wff 𝐴 Fn 𝐵
41wfun 5870 . . 3 wff Fun 𝐴
51cdm 5104 . . . 4 class dom 𝐴
65, 2wceq 1481 . . 3 wff dom 𝐴 = 𝐵
74, 6wa 384 . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
83, 7wb 196 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  funfn  5906  fnsng  5926  fnprg  5935  fntpg  5936  fntp  5937  fncnv  5950  fneq1  5967  fneq2  5968  nffn  5975  fnfun  5976  fndm  5978  fnun  5985  fnco  5987  fnssresb  5991  fnres  5995  fnresi  5996  fn0  5998  mptfnf  6002  fnopabg  6004  sbcfng  6029  fdmrn  6051  fcoi1  6065  f00  6074  f1cnvcnv  6096  fores  6111  dff1o4  6132  foimacnv  6141  funfv  6252  fvimacnvALT  6322  respreima  6330  dff3  6358  fpr  6406  fnsnb  6417  fnprb  6457  fnex  6466  fliftf  6550  fnoprabg  6746  fun11iun  7111  f1oweALT  7137  curry1  7254  curry2  7257  tposfn2  7359  wfrlem13  7412  wfr1  7418  tfrlem10  7468  tfr1  7478  frfnom  7515  undifixp  7929  sbthlem9  8063  fodomr  8096  rankf  8642  cardf2  8754  axdc3lem2  9258  nqerf  9737  axaddf  9951  axmulf  9952  uzrdgfni  12740  hashkf  13102  shftfn  13794  imasaddfnlem  16169  imasvscafn  16178  fntopon  20709  cnextf  21851  ftc1cn  23787  grporn  27345  ffsrn  29478  measdivcstOLD  30261  bnj145OLD  30769  bnj1422  30882  nofnbday  31779  elno2  31781  scutf  31893  fnsingle  32001  fnimage  32011  imageval  32012  dfrecs2  32032  dfrdg4  32033  ftc1cnnc  33455  fnresfnco  40969  funcoressn  40970  afvco2  41019
  Copyright terms: Public domain W3C validator