Theorem funfnd 6379

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

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

Syntax hints:   → wi 4  dom cdm 5548  Fun wfun 6342   Fn wfn 6343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812  df-fn 6351

This theorem is referenced by:  resfunexg  6970  funiunfv  6999  funelss  7738  funsssuppss  7848  wfrlem4  7950  smores2  7983  tfrlem1  8004  resfnfinfin  8796  resfifsupp  8853  ordtypelem4  8977  ordtypelem9  8982  ordtypelem10  8983  brdom3  9942  brdom5  9943  brdom4  9944  fpwwe2lem11  10054  hashimarn  13793  resunimafz0  13795  isstruct2  16485  invf  17030  lindfrn  20957  ofco2  21052  dfac14  22218  perfdvf  24493  c1lip2  24587  taylf  24941  lpvtx  26845  upgrle2  26882  uhgrvtxedgiedgb  26913  uhgr2edg  26982  ushgredgedg  27003  ushgredgedgloop  27005  subgruhgredgd  27058  subuhgr  27060  subupgr  27061  subumgr  27062  subusgr  27063  upgrres  27080  umgrres  27081  vtxdun  27255  upgrewlkle2  27380  eupthvdres  28006  cycpmfvlem  30747  cycpmfv3  30750  sitgf  31598  frrlem4  33119  elno2  33154  gneispace  40475  gneispacef2  40477  funimaeq  41508  limsupresxr  42037  liminfresxr  42038  funcoressn  43268