Theorem funfnd 6548

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 6547	. 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
3	1, 2	sylib 220	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

Syntax hints:   → wi 4  dom cdm 5645  Fun wfun 6511   Fn wfn 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-fn 6520

This theorem is referenced by:  fncofn  6634  resfunexg  7195  ralima  7217  funiunfv  7228  funelss  8024  funsssuppss  8165  frrlem4  8265  smores2  8320  tfrlem1  8341  resfnfinfin  9277  resfifsupp  9340  ordtypelem4  9466  ordtypelem9  9471  ordtypelem10  9472  brdom3  10482  brdom5  10483  brdom4  10484  fpwwe2lem10  10595  hashimarn  14450  resunimafz0  14455  isstruct2  17168  invf  17784  lindfrn  21853  psdmul  22211  ofco2  22491  dfac14  23658  perfdvf  25945  c1lip2  26040  taylf  26401  elno2  27695  noinfbnd2lem1  27771  noetainflem4  27781  lpvtx  29215  upgrle2  29252  uhgrvtxedgiedgb  29283  uhgr2edg  29355  ushgredgedg  29376  ushgredgedgloop  29378  subgruhgredgd  29431  subuhgr  29433  subupgr  29434  subumgr  29435  subusgr  29436  upgrres  29453  umgrres  29454  vtxdun  29628  upgrewlkle2  29753  eupthvdres  30383  cycpmfvlem  33253  cycpmfv3  33256  sitgf  34605  cardpred  35352  nummin  35353  bj-gabima  37389  gneispace  44674  gneispacef2  44676  funimaeq  45785  limsupresxr  46304  liminfresxr  46305  funcoressn  47600  isubgr0uhgr  48459  upgrimwlklem1  48483