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

Theorem funfnd 6385
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 6384 . 2 (Fun 𝐴𝐴 Fn dom 𝐴)
31, 2sylib 220 1 (𝜑𝐴 Fn dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  dom cdm 5554  Fun wfun 6348   Fn wfn 6349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-fn 6357
This theorem is referenced by:  resfunexg  6977  funiunfv  7006  funelss  7745  funsssuppss  7855  wfrlem4  7957  smores2  7990  tfrlem1  8011  resfnfinfin  8803  resfifsupp  8860  ordtypelem4  8984  ordtypelem9  8989  ordtypelem10  8990  brdom3  9949  brdom5  9950  brdom4  9951  fpwwe2lem11  10061  hashimarn  13800  resunimafz0  13802  isstruct2  16492  invf  17037  lindfrn  20964  ofco2  21059  dfac14  22225  perfdvf  24500  c1lip2  24594  taylf  24948  lpvtx  26852  upgrle2  26889  uhgrvtxedgiedgb  26920  uhgr2edg  26989  ushgredgedg  27010  ushgredgedgloop  27012  subgruhgredgd  27065  subuhgr  27067  subupgr  27068  subumgr  27069  subusgr  27070  upgrres  27087  umgrres  27088  vtxdun  27262  upgrewlkle2  27387  eupthvdres  28013  cycpmfvlem  30754  cycpmfv3  30757  sitgf  31605  frrlem4  33126  elno2  33161  gneispace  40482  gneispacef2  40484  funimaeq  41516  limsupresxr  42045  liminfresxr  42046  funcoressn  43276
  Copyright terms: Public domain W3C validator