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

Definition df-fn 6346
 Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6505, dffn3 6515, dffn4 6587, and dffn5 6715. (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 6338 . 2 wff 𝐴 Fn 𝐵
41wfun 6337 . . 3 wff Fun 𝐴
51cdm 5542 . . . 4 class dom 𝐴
65, 2wceq 1538 . . 3 wff dom 𝐴 = 𝐵
74, 6wa 399 . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
83, 7wb 209 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
 Colors of variables: wff setvar class This definition is referenced by:  funfn  6373  fnsng  6394  fnprg  6401  fntpg  6402  fntp  6403  fncnv  6415  fneq1  6432  fneq2  6433  nffn  6440  fnfun  6441  fndm  6443  fnun  6452  fnco  6454  fnssresb  6458  fnres  6463  idfn  6464  fnresiOLD  6466  fn0  6468  mptfnf  6472  fnopabg  6474  sbcfng  6500  fdmrn  6528  fcoi1  6542  f00  6551  f1cnvcnv  6575  fores  6591  dff1o4  6614  foimacnv  6623  funfv  6741  fvimacnvALT  6818  respreima  6827  dff3  6857  fpr  6907  fnsnb  6919  fnprb  6962  fnex  6971  fliftf  7061  fnoprabg  7268  fiun  7639  f1iun  7640  f1oweALT  7668  curry1  7795  curry2  7798  tposfn2  7910  wfrlem13  7963  wfr1  7969  tfrlem10  8019  tfr1  8029  frfnom  8066  undifixp  8494  sbthlem9  8632  fodomr  8665  rankf  9220  cardf2  9369  axdc3lem2  9871  nqerf  10350  axaddf  10565  axmulf  10566  uzrdgfni  13330  hashkf  13697  shftfn  14432  imasaddfnlem  16801  imasvscafn  16810  fntopon  21536  cnextf  22678  ftc1cn  24653  grporn  28311  ffsrn  30480  measdivcstALTV  31545  bnj1422  32170  satff  32718  frrlem11  33194  frrlem12  33195  fpr1  33200  frr1  33205  nofnbday  33220  scutf  33334  fnsingle  33441  fnimage  33451  imageval  33452  dfrecs2  33472  dfrdg4  33473  ftc1cnnc  35078  fnresfnco  43564  funcoressn  43565  afvco2  43663
 Copyright terms: Public domain W3C validator