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

Theorem funfnd 6533
Description: A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypothesis
Ref Expression
funfnd.1 (𝜑 → Fun 𝐴)
Assertion
Ref Expression
funfnd (𝜑𝐴 Fn dom 𝐴)

Proof of Theorem funfnd
StepHypRef Expression
1 funfnd.1 . 2 (𝜑 → Fun 𝐴)
2 funfn 6532 . 2 (Fun 𝐴𝐴 Fn dom 𝐴)
31, 2sylib 217 1 (𝜑𝐴 Fn dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  dom cdm 5634  Fun wfun 6491   Fn wfn 6492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6500
This theorem is referenced by:  fncofn  6618  resfunexg  7166  funiunfv  7196  funelss  7980  funsssuppss  8122  frrlem4  8221  wfrlem4OLD  8259  smores2  8301  tfrlem1  8323  resfnfinfin  9279  resfifsupp  9338  ordtypelem4  9462  ordtypelem9  9467  ordtypelem10  9468  brdom3  10469  brdom5  10470  brdom4  10471  fpwwe2lem10  10581  hashimarn  14346  resunimafz0  14348  isstruct2  17026  invf  17656  lindfrn  21243  ofco2  21816  dfac14  22985  perfdvf  25283  c1lip2  25378  taylf  25736  elno2  27018  noinfbnd2lem1  27094  noetainflem4  27104  lpvtx  28061  upgrle2  28098  uhgrvtxedgiedgb  28129  uhgr2edg  28198  ushgredgedg  28219  ushgredgedgloop  28221  subgruhgredgd  28274  subuhgr  28276  subupgr  28277  subumgr  28278  subusgr  28279  upgrres  28296  umgrres  28297  vtxdun  28471  upgrewlkle2  28596  eupthvdres  29221  cycpmfvlem  32010  cycpmfv3  32013  sitgf  33004  cardpred  33751  nummin  33752  bj-gabima  35456  gneispace  42494  gneispacef2  42496  funimaeq  43561  limsupresxr  44093  liminfresxr  44094  funcoressn  45362
  Copyright terms: Public domain W3C validator