Theorem fnfun 6650

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5677  Fun wfun 6538   Fn wfn 6539

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 206  df-an 398  df-fn 6547

This theorem is referenced by:  fnfund  6651  fnrel  6652  funfni  6656  fncofn  6667  fnco  6668  fncoOLD  6669  fnssresb  6673  ffun  6721  f1fun  6790  f1ofun  6836  fnbrfvb  6945  fvelimad  6960  fvelimab  6965  fvun1  6983  elpreima  7060  respreima  7068  rescnvimafod  7076  fnsnr  7163  fnprb  7210  fntpb  7211  fconst3  7215  fnfvima  7235  fnunirn  7253  nvof1o  7278  f1eqcocnv  7299  f1eqcocnvOLD  7300  offun  7684  fnexALT  7937  curry1  8090  curry2  8093  fimaproj  8121  suppvalfng  8153  suppvalfn  8154  suppfnss  8174  fnsuppres  8176  frrlem2  8272  frrlem12  8282  wfrlem2OLD  8309  wfrlem14OLD  8322  tfrlem4  8379  tfrlem5  8380  tfrlem11  8388  tz7.48-2  8442  tz7.49  8445  naddcllem  8675  naddov2  8678  naddunif  8692  naddasslem1  8693  naddasslem2  8694  fndmeng  9035  fnfi  9181  fodomfi  9325  resfnfinfin  9332  fczfsuppd  9381  marypha2lem4  9433  inf0  9616  r1elss  9801  dfac8alem  10024  alephfp  10103  dfac3  10116  dfac9  10131  dfac12lem1  10138  dfac12lem2  10139  r1om  10239  cfsmolem  10265  alephsing  10271  zorn2lem1  10491  zorn2lem5  10495  zorn2lem6  10496  zorn2lem7  10497  ttukeylem3  10506  ttukeylem6  10509  fnct  10532  smobeth  10581  fpwwe2lem8  10633  wunr1om  10714  tskr1om  10762  tskr1om2  10763  uzrdg0i  13924  uzrdgsuci  13925  seqexw  13982  hashkf  14292  cshimadifsn  14780  cshimadifsn0  14781  shftfn  15020  phimullem  16712  imasaddvallem  17475  imasvscaval  17484  lidlval  20814  rspval  20815  psgnghm  21133  iscldtop  22599  2ndcomap  22962  qtoptop  23204  basqtop  23215  qtoprest  23221  kqfvima  23234  isr0  23241  kqreglem1  23245  kqnrmlem1  23247  kqnrmlem2  23248  ustbas  23732  uniiccdif  25095  noextendseq  27170  madeval  27347  oldval  27349  addsval  27446  negsval  27500  negsproplem2  27503  negsunif  27529  mulsval  27565  fcoinver  31835  fnpreimac  31896  mdetpmtr1  32803  sseqf  33391  sseqfv2  33393  elorrvc  33462  bnj1371  34040  bnj1497  34071  fnrelpredd  34092  filnetlem4  35266  heibor1lem  36677  diaf11N  39920  dibf11N  40032  dibclN  40033  dihintcl  40215  fnsnbt  41051  ismrc  41439  dnnumch1  41786  aomclem4  41799  aomclem6  41801  tfsconcatrev  42098  tfsnfin  42102  fnimafnex  42191  ntrclsfv1  42806  ntrneifv1  42830  finnzfsuppd  42961  fvelima2  43964  climrescn  44464  icccncfext  44603  stoweidlem29  44745  stoweidlem59  44775  ovolval4lem1  45365  fnresfnco  45751  funcoressn  45752  fnfocofob  45787  fnbrafvb  45862  tz6.12-afv  45881  afvco2  45884  tz6.12-afv2  45948  fnbrafv2b  45956  imaelsetpreimafv  46063  imasetpreimafvbijlemfv  46070  imasetpreimafvbijlemfo  46073  plusfreseq  46542  dfrngc2  46870  dfringc2  46916  rngcresringcat  46928  ackvalsuc0val  47373