Theorem funfnd 6563

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

This proof depends on syntax axioms:   → wi 4  dom cdm 5651  Fun wfun 6525   Fn wfn 6526

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-fn 6534

This theorem is used by:  fncofn  6648  resfunexg  7213  ralima  7235  funiunfv  7244  funelss  8047  funsssuppss  8191  frrlem4  8291  smores2  8346  tfrlem1  8367  resfnfinfin  9310  resfifsupp  9373  ordtypelem4  9499  ordtypelem9  9504  ordtypelem10  9505  brdom3  10588  brdom5  10589  brdom4  10590  fpwwe2lem10  10706  hashimarn  14565  resunimafz0  14570  isstruct2  17307  invf  17923  lindfrn  22107  psdmul  22467  ofco2  22746  dfac14  23917  perfdvf  26203  c1lip2  26298  taylf  26670  elno2  27993  noinfbnd2lem1  28069  noetainflem4  28079  lpvtx  29628  upgrle2  29665  uhgrvtxedgiedgb  29696  uhgr2edg  29771  ushgredgedg  29792  ushgredgedgloop  29794  subgruhgredgd  29847  subuhgr  29849  subupgr  29850  subumgr  29851  subusgr  29852  upgrres  29869  umgrres  29870  vtxdun  30044  upgrewlkle2  30169  eupthvdres  30818  cycpmfvlem  33655  cycpmfv3  33658  sitgf  34962  cardpred  35700  nummin  35701  bj-gabima  37823  gneispace  45093  gneispacef2  45095  funimaeq  46201  limsupresxr  46720  liminfresxr  46721  funcoressn  48056  isubgr0uhgr  48915  upgrimwlklem1  48939