Theorem fnfun 6280

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

Syntax hints:   → wi 4   = wceq 1507  dom cdm 5401  Fun wfun 6176   Fn wfn 6177

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 199  df-an 388  df-fn 6185

This theorem is referenced by:  fnrel  6281  funfni  6284  fnco  6292  fnssresb  6296  ffun  6341  f1fun  6400  f1ofun  6440  fnbrfvb  6542  fvelimab  6560  fvun1  6576  elpreima  6647  respreima  6655  fnsnr  6744  fnprb  6791  fntpb  6792  fconst3  6796  fnfvima  6814  fnunirn  6831  nvof1o  6856  f1eqcocnv  6876  fnexALT  7458  curry1  7601  curry2  7604  suppvalfn  7634  suppfnss  7652  fnsuppres  7654  wfrlem2  7752  wfrlem14  7766  tfrlem4  7813  tfrlem5  7814  tfrlem11  7822  tz7.48-2  7875  tz7.49  7878  fndmeng  8378  fnfi  8585  fodomfi  8586  resfnfinfin  8593  fczfsuppd  8640  marypha2lem4  8691  inf0  8872  r1elss  9023  dfac8alem  9243  alephfp  9322  dfac3  9335  dfac9  9350  dfac12lem1  9357  dfac12lem2  9358  r1om  9458  cfsmolem  9484  alephsing  9490  zorn2lem1  9710  zorn2lem5  9714  zorn2lem6  9715  zorn2lem7  9716  ttukeylem3  9725  ttukeylem6  9728  fnct  9751  smobeth  9800  fpwwe2lem9  9852  wunr1om  9933  tskr1om  9981  tskr1om2  9982  uzrdg0i  13136  uzrdgsuci  13137  seqexw  13194  hashkf  13501  cshimadifsn  14047  cshimadifsn0  14048  shftfn  14287  phimullem  15966  imasaddvallem  16652  imasvscaval  16661  lcomfsupp  19390  lidlval  19680  rspval  19681  psrbagev1  19997  psgnghm  20420  frlmsslsp  20636  iscldtop  21401  2ndcomap  21764  qtoptop  22006  basqtop  22017  qtoprest  22023  kqfvima  22036  isr0  22043  kqreglem1  22047  kqnrmlem1  22049  kqnrmlem2  22050  elrnust  22530  ustbas  22533  uniiccdif  23876  fcoinver  30115  fnpreimac  30172  mdetpmtr1  30730  fimaproj  30741  sseqf  31296  sseqfv2  31298  elorrvc  31367  bnj930  31689  bnj1371  31946  bnj1497  31977  frrlem2  32645  frrlem12  32655  noextendseq  32695  madeval  32810  filnetlem4  33250  heibor1lem  34529  diaf11N  37630  dibf11N  37742  dibclN  37743  dihintcl  37925  fnsnbt  38565  ismrc  38693  dnnumch1  39040  aomclem4  39053  aomclem6  39055  ntrclsfv1  39768  ntrneifv1  39792  fvelimad  40945  fvelima2  40960  climrescn  41460  icccncfext  41600  stoweidlem29  41745  stoweidlem59  41775  ovolval4lem1  42362  fnresfnco  42681  funcoressn  42682  fnbrafvb  42759  tz6.12-afv  42778  afvco2  42781  tz6.12-afv2  42845  fnbrafv2b  42853  plusfreseq  43407  dfrngc2  43607  dfringc2  43653  rngcresringcat  43665  mndpsuppss  43785  mndpfsupp  43790