Theorem fnfun 6479

Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fnfun	⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Proof of Theorem fnfun

Step	Hyp	Ref	Expression
1		df-fn 6383	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simplbi 501	1 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Syntax hints:   → wi 4   = wceq 1543  dom cdm 5551  Fun wfun 6374   Fn wfn 6375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-fn 6383

This theorem is referenced by:  fnrel  6480  funfni  6484  fncofn  6493  fnco  6494  fncoOLD  6495  fnssresb  6499  ffun  6548  f1fun  6617  f1ofun  6663  fnbrfvb  6765  fvelimad  6779  fvelimab  6784  fvun1  6802  elpreima  6878  respreima  6886  rescnvimafod  6894  fnsnr  6980  fnprb  7024  fntpb  7025  fconst3  7029  fnfvima  7049  fnunirn  7066  nvof1o  7091  f1eqcocnv  7111  f1eqcocnvOLD  7112  offun  7482  fnexALT  7724  curry1  7872  curry2  7875  fimaproj  7902  suppvalfng  7910  suppvalfn  7911  suppfnss  7931  fnsuppres  7933  frrlem2  8028  frrlem12  8038  wfrlem2  8055  wfrlem14  8068  tfrlem4  8115  tfrlem5  8116  tfrlem11  8124  tz7.48-2  8178  tz7.49  8181  fndmeng  8712  fnfi  8858  fodomfi  8949  resfnfinfin  8956  fczfsuppd  9003  marypha2lem4  9054  inf0  9236  r1elss  9422  dfac8alem  9643  alephfp  9722  dfac3  9735  dfac9  9750  dfac12lem1  9757  dfac12lem2  9758  r1om  9858  cfsmolem  9884  alephsing  9890  zorn2lem1  10110  zorn2lem5  10114  zorn2lem6  10115  zorn2lem7  10116  ttukeylem3  10125  ttukeylem6  10128  fnct  10151  smobeth  10200  fpwwe2lem8  10252  wunr1om  10333  tskr1om  10381  tskr1om2  10382  uzrdg0i  13532  uzrdgsuci  13533  seqexw  13590  hashkf  13898  cshimadifsn  14394  cshimadifsn0  14395  shftfn  14636  phimullem  16332  imasaddvallem  17034  imasvscaval  17043  lidlval  20229  rspval  20230  psgnghm  20542  iscldtop  21992  2ndcomap  22355  qtoptop  22597  basqtop  22608  qtoprest  22614  kqfvima  22627  isr0  22634  kqreglem1  22638  kqnrmlem1  22640  kqnrmlem2  22641  elrnust  23122  ustbas  23125  uniiccdif  24475  fcoinver  30665  fnpreimac  30728  mdetpmtr1  31487  sseqf  32071  sseqfv2  32073  elorrvc  32142  bnj930  32462  bnj1371  32722  bnj1497  32753  fnrelpredd  32774  naddcllem  33568  naddov2  33571  noextendseq  33607  madeval  33773  oldval  33775  negsval  33860  addsval  33863  filnetlem4  34307  heibor1lem  35704  diaf11N  38800  dibf11N  38912  dibclN  38913  dihintcl  39095  fnsnbt  39921  ismrc  40226  dnnumch1  40572  aomclem4  40585  aomclem6  40587  ntrclsfv1  41342  ntrneifv1  41366  finnzfsuppd  41498  fvelima2  42478  climrescn  42964  icccncfext  43103  stoweidlem29  43245  stoweidlem59  43275  ovolval4lem1  43862  fnresfnco  44207  funcoressn  44208  fnfocofob  44243  fnbrafvb  44318  tz6.12-afv  44337  afvco2  44340  tz6.12-afv2  44404  fnbrafv2b  44412  imaelsetpreimafv  44520  imasetpreimafvbijlemfv  44527  imasetpreimafvbijlemfo  44530  plusfreseq  44999  dfrngc2  45203  dfringc2  45249  rngcresringcat  45261  ackvalsuc0val  45706