Theorem funfnd 6547

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

Syntax hints:   → wi 4  dom cdm 5638  Fun wfun 6505   Fn wfn 6506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6514

This theorem is referenced by:  fncofn  6635  resfunexg  7189  ralima  7211  funiunfv  7222  funelss  8026  funsssuppss  8169  frrlem4  8268  smores2  8323  tfrlem1  8344  resfnfinfin  9288  resfifsupp  9348  ordtypelem4  9474  ordtypelem9  9479  ordtypelem10  9480  brdom3  10481  brdom5  10482  brdom4  10483  fpwwe2lem10  10593  hashimarn  14405  resunimafz0  14410  isstruct2  17119  invf  17730  lindfrn  21730  psdmul  22053  ofco2  22338  dfac14  23505  perfdvf  25804  c1lip2  25903  taylf  26268  elno2  27566  noinfbnd2lem1  27642  noetainflem4  27652  lpvtx  28995  upgrle2  29032  uhgrvtxedgiedgb  29063  uhgr2edg  29135  ushgredgedg  29156  ushgredgedgloop  29158  subgruhgredgd  29211  subuhgr  29213  subupgr  29214  subumgr  29215  subusgr  29216  upgrres  29233  umgrres  29234  vtxdun  29409  upgrewlkle2  29534  eupthvdres  30164  cycpmfvlem  33069  cycpmfv3  33072  sitgf  34338  cardpred  35080  nummin  35081  bj-gabima  36928  gneispace  44123  gneispacef2  44125  funimaeq  45240  limsupresxr  45764  liminfresxr  45765  funcoressn  47043  isubgr0uhgr  47873  upgrimwlklem1  47897