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

Theorem funfnd 6166
Description: A function is a function over 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 6165 . 2 (Fun 𝐴𝐴 Fn dom 𝐴)
31, 2sylib 210 1 (𝜑𝐴 Fn dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  dom cdm 5355  Fun wfun 6129   Fn wfn 6130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-fn 6138
This theorem is referenced by:  resfunexg  6751  funiunfv  6778  funsssuppss  7603  wfrlem4  7700  smores2  7734  tfrlem1  7755  resfnfinfin  8534  resfifsupp  8591  ordtypelem4  8715  ordtypelem9  8720  ordtypelem10  8721  brdom3  9685  brdom5  9686  brdom4  9687  fpwwe2lem11  9797  hashimarn  13541  resunimafz0  13543  isstruct2  16265  invf  16813  uhgrvtxedgiedgb  26484  ushgredgedgloop  26577  upgrres  26653  umgrres  26654  funimaeq  40372  limsupresxr  40906  liminfresxr  40907
  Copyright terms: Public domain W3C validator