Theorem fnfun 6598

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 6501	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simplbi 496	1 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5631  Fun wfun 6492   Fn wfn 6493

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 207  df-an 396  df-fn 6501

This theorem is referenced by:  fnfund  6599  fnrel  6600  funfni  6604  fncofn  6615  fnco  6616  fnssresb  6620  ffun  6671  f1fun  6738  f1ofun  6782  fnbrfvb  6890  fvelima2  6892  fvelimad  6907  fvelimab  6912  fvun1  6931  elpreima  7010  respreima  7018  rescnvimafod  7025  fnsnr  7118  fnsnbg  7119  fnprb  7163  fntpb  7164  fconst3  7168  fnfvima  7188  ralima  7192  fnunirn  7208  nvof1o  7235  f1eqcocnv  7256  offun  7645  fnexALT  7904  curry1  8054  curry2  8057  fimaproj  8085  suppvalfng  8117  suppvalfn  8118  suppfnss  8139  fnsuppres  8141  frrlem2  8237  frrlem12  8247  tfrlem4  8318  tfrlem5  8319  tfrlem11  8327  tz7.48-2  8381  tz7.49  8384  naddcllem  8612  naddov2  8615  naddunif  8629  naddasslem1  8630  naddasslem2  8631  fndmeng  8982  fnfi  9112  fodomfi  9222  fodomfiOLD  9240  resfnfinfin  9247  tfsnfin2  9273  finnzfsuppd  9286  fczfsuppd  9299  marypha2lem4  9351  inf0  9542  r1elss  9730  dfac8alem  9951  alephfp  10030  dfac3  10043  dfac9  10059  dfac12lem1  10066  dfac12lem2  10067  r1om  10165  cfsmolem  10192  alephsing  10198  zorn2lem1  10418  zorn2lem5  10422  zorn2lem6  10423  zorn2lem7  10424  ttukeylem3  10433  ttukeylem6  10436  fnct  10459  smobeth  10509  fpwwe2lem8  10561  wunr1om  10642  tskr1om  10690  tskr1om2  10691  uzrdg0i  13921  uzrdgsuci  13922  seqexw  13979  hashkf  14294  cshimadifsn  14791  cshimadifsn0  14792  shftfn  15035  phimullem  16749  imasaddvallem  17493  imasvscaval  17502  dfrngc2  20605  dfringc2  20634  rngcresringcat  20646  lidlval  21208  rspval  21209  psgnghm  21560  iscldtop  23060  2ndcomap  23423  qtoptop  23665  basqtop  23676  qtoprest  23682  kqfvima  23695  isr0  23702  kqreglem1  23706  kqnrmlem1  23708  kqnrmlem2  23709  ustbas  24192  uniiccdif  25545  noextendseq  27631  madeval  27824  oldval  27826  addsval  27954  negsval  28017  negsproplem2  28021  negsunif  28047  mulsval  28101  zsex  28372  nowisdomv  30544  fcoinver  32674  fresunsn  32698  fnpreimac  32743  elrgspnlem2  33304  mdetpmtr1  33967  sseqf  34536  sseqfv2  34538  elorrvc  34608  bnj1371  35171  bnj1497  35202  fnrelpredd  35234  gblacfnacd  35284  onvf1odlem3  35287  onvf1odlem4  35288  onvf1od  35289  filnetlem4  36563  heibor1lem  38130  diaf11N  41495  dibf11N  41607  dibclN  41608  dihintcl  41790  aks6d1c2lem4  42566  ismrc  43133  dnnumch1  43472  aomclem4  43485  aomclem6  43487  tfsconcatrev  43776  tfsnfin  43780  fnimafnex  43867  ntrclsfv1  44482  ntrneifv1  44506  climrescn  46176  icccncfext  46315  stoweidlem29  46457  stoweidlem59  46487  ovolval4lem1  47077  fnresfnco  47489  funcoressn  47490  fnfocofob  47527  fnbrafvb  47602  tz6.12-afv  47621  afvco2  47624  tz6.12-afv2  47688  fnbrafv2b  47696  imaelsetpreimafv  47855  imasetpreimafvbijlemfv  47862  imasetpreimafvbijlemfo  47865  plusfreseq  48640  ackvalsuc0val  49163