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

Step	Hyp	Ref	Expression
1		funfnd.1	. 2 ⊢ (𝜑 → Fun 𝐴)
2		funfn 6165	. 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
3	1, 2	sylib 210	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

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