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

Theorem funfnd 6530
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 6529 . 2 (Fun 𝐴𝐴 Fn dom 𝐴)
31, 2sylib 217 1 (𝜑𝐴 Fn dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  dom cdm 5632  Fun wfun 6488   Fn wfn 6489
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728  df-fn 6497
This theorem is referenced by:  fncofn  6615  resfunexg  7162  funiunfv  7192  funelss  7976  funsssuppss  8118  frrlem4  8217  wfrlem4OLD  8255  smores2  8297  tfrlem1  8319  resfnfinfin  9273  resfifsupp  9330  ordtypelem4  9454  ordtypelem9  9459  ordtypelem10  9460  brdom3  10461  brdom5  10462  brdom4  10463  fpwwe2lem10  10573  hashimarn  14337  resunimafz0  14339  isstruct2  17018  invf  17648  lindfrn  21223  ofco2  21796  dfac14  22965  perfdvf  25263  c1lip2  25358  taylf  25716  elno2  26998  noinfbnd2lem1  27074  noetainflem4  27084  lpvtx  27917  upgrle2  27954  uhgrvtxedgiedgb  27985  uhgr2edg  28054  ushgredgedg  28075  ushgredgedgloop  28077  subgruhgredgd  28130  subuhgr  28132  subupgr  28133  subumgr  28134  subusgr  28135  upgrres  28152  umgrres  28153  vtxdun  28327  upgrewlkle2  28452  eupthvdres  29077  cycpmfvlem  31856  cycpmfv3  31859  sitgf  32838  cardpred  33585  nummin  33586  bj-gabima  35399  gneispace  42386  gneispacef2  42388  funimaeq  43448  limsupresxr  43977  liminfresxr  43978  funcoressn  45246
  Copyright terms: Public domain W3C validator