Theorem fnfun 6648

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

Syntax hints:   → wi 4   = wceq 1534  dom cdm 5672  Fun wfun 6536   Fn wfn 6537

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 396  df-fn 6545

This theorem is referenced by:  fnfund  6649  fnrel  6650  funfni  6654  fncofn  6665  fnco  6666  fncoOLD  6667  fnssresb  6671  ffun  6719  f1fun  6789  f1ofun  6835  fnbrfvb  6944  fvelimad  6960  fvelimab  6965  fvun1  6983  elpreima  7061  respreima  7069  rescnvimafod  7077  fnsnr  7168  fnprb  7214  fntpb  7215  fconst3  7219  fnfvima  7239  fnunirn  7258  nvof1o  7283  f1eqcocnv  7304  f1eqcocnvOLD  7305  offun  7693  fnexALT  7948  curry1  8103  curry2  8106  fimaproj  8134  suppvalfng  8166  suppvalfn  8167  suppfnss  8187  fnsuppres  8189  frrlem2  8286  frrlem12  8296  wfrlem2OLD  8323  wfrlem14OLD  8336  tfrlem4  8393  tfrlem5  8394  tfrlem11  8402  tz7.48-2  8456  tz7.49  8459  naddcllem  8690  naddov2  8693  naddunif  8707  naddasslem1  8708  naddasslem2  8709  fndmeng  9051  fnfi  9197  fodomfi  9341  resfnfinfin  9348  fczfsuppd  9401  marypha2lem4  9453  inf0  9636  r1elss  9821  dfac8alem  10044  alephfp  10123  dfac3  10136  dfac9  10151  dfac12lem1  10158  dfac12lem2  10159  r1om  10259  cfsmolem  10285  alephsing  10291  zorn2lem1  10511  zorn2lem5  10515  zorn2lem6  10516  zorn2lem7  10517  ttukeylem3  10526  ttukeylem6  10529  fnct  10552  smobeth  10601  fpwwe2lem8  10653  wunr1om  10734  tskr1om  10782  tskr1om2  10783  uzrdg0i  13948  uzrdgsuci  13949  seqexw  14006  hashkf  14315  cshimadifsn  14804  cshimadifsn0  14805  shftfn  15044  phimullem  16739  imasaddvallem  17502  imasvscaval  17511  dfrngc2  20550  dfringc2  20579  rngcresringcat  20591  lidlval  21095  rspval  21096  psgnghm  21499  iscldtop  22986  2ndcomap  23349  qtoptop  23591  basqtop  23602  qtoprest  23608  kqfvima  23621  isr0  23628  kqreglem1  23632  kqnrmlem1  23634  kqnrmlem2  23635  ustbas  24119  uniiccdif  25494  noextendseq  27587  madeval  27766  oldval  27768  addsval  27866  negsval  27925  negsproplem2  27928  negsunif  27954  mulsval  27996  fcoinver  32379  fnpreimac  32440  mdetpmtr1  33360  sseqf  33948  sseqfv2  33950  elorrvc  34019  bnj1371  34596  bnj1497  34627  fnrelpredd  34648  filnetlem4  35801  heibor1lem  37217  diaf11N  40459  dibf11N  40571  dibclN  40572  dihintcl  40754  aks6d1c2lem4  41530  fnsnbt  41641  ismrc  42043  dnnumch1  42390  aomclem4  42403  aomclem6  42405  tfsconcatrev  42700  tfsnfin  42704  fnimafnex  42793  ntrclsfv1  43408  ntrneifv1  43432  finnzfsuppd  43562  fvelima2  44559  climrescn  45059  icccncfext  45198  stoweidlem29  45340  stoweidlem59  45370  ovolval4lem1  45960  fnresfnco  46346  funcoressn  46347  fnfocofob  46382  fnbrafvb  46457  tz6.12-afv  46476  afvco2  46479  tz6.12-afv2  46543  fnbrafv2b  46551  imaelsetpreimafv  46658  imasetpreimafvbijlemfv  46665  imasetpreimafvbijlemfo  46668  plusfreseq  47149  ackvalsuc0val  47683