Theorem fnfun 6592

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5624  Fun wfun 6486   Fn wfn 6487

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 6495

This theorem is referenced by:  fnfund  6593  fnrel  6594  funfni  6598  fncofn  6609  fnco  6610  fnssresb  6614  ffun  6665  f1fun  6732  f1ofun  6776  fnbrfvb  6884  fvelima2  6886  fvelimad  6901  fvelimab  6906  fvun1  6925  elpreima  7004  respreima  7012  rescnvimafod  7019  fnsnr  7111  fnsnbg  7112  fnprb  7156  fntpb  7157  fconst3  7161  fnfvima  7181  ralima  7185  fnunirn  7201  nvof1o  7228  f1eqcocnv  7249  offun  7638  fnexALT  7897  curry1  8047  curry2  8050  fimaproj  8078  suppvalfng  8110  suppvalfn  8111  suppfnss  8132  fnsuppres  8134  frrlem2  8230  frrlem12  8240  tfrlem4  8311  tfrlem5  8312  tfrlem11  8320  tz7.48-2  8374  tz7.49  8377  naddcllem  8605  naddov2  8608  naddunif  8622  naddasslem1  8623  naddasslem2  8624  fndmeng  8975  fnfi  9105  fodomfi  9215  fodomfiOLD  9233  resfnfinfin  9240  tfsnfin2  9266  finnzfsuppd  9279  fczfsuppd  9292  marypha2lem4  9344  inf0  9533  r1elss  9721  dfac8alem  9942  alephfp  10021  dfac3  10034  dfac9  10050  dfac12lem1  10057  dfac12lem2  10058  r1om  10156  cfsmolem  10183  alephsing  10189  zorn2lem1  10409  zorn2lem5  10413  zorn2lem6  10414  zorn2lem7  10415  ttukeylem3  10424  ttukeylem6  10427  fnct  10450  smobeth  10500  fpwwe2lem8  10552  wunr1om  10633  tskr1om  10681  tskr1om2  10682  uzrdg0i  13912  uzrdgsuci  13913  seqexw  13970  hashkf  14285  cshimadifsn  14782  cshimadifsn0  14783  shftfn  15026  phimullem  16740  imasaddvallem  17484  imasvscaval  17493  dfrngc2  20596  dfringc2  20625  rngcresringcat  20637  lidlval  21200  rspval  21201  psgnghm  21570  iscldtop  23070  2ndcomap  23433  qtoptop  23675  basqtop  23686  qtoprest  23692  kqfvima  23705  isr0  23712  kqreglem1  23716  kqnrmlem1  23718  kqnrmlem2  23719  ustbas  24202  uniiccdif  25555  noextendseq  27645  madeval  27838  oldval  27840  addsval  27968  negsval  28031  negsproplem2  28035  negsunif  28061  mulsval  28115  zsex  28386  nowisdomv  30559  fcoinver  32689  fresunsn  32713  fnpreimac  32758  elrgspnlem2  33319  mdetpmtr1  33983  sseqf  34552  sseqfv2  34554  elorrvc  34624  bnj1371  35187  bnj1497  35218  fnrelpredd  35250  gblacfnacd  35300  onvf1odlem3  35303  onvf1odlem4  35304  onvf1od  35305  filnetlem4  36579  heibor1lem  38144  diaf11N  41509  dibf11N  41621  dibclN  41622  dihintcl  41804  aks6d1c2lem4  42580  ismrc  43147  dnnumch1  43490  aomclem4  43503  aomclem6  43505  tfsconcatrev  43794  tfsnfin  43798  fnimafnex  43885  ntrclsfv1  44500  ntrneifv1  44524  climrescn  46194  icccncfext  46333  stoweidlem29  46475  stoweidlem59  46505  ovolval4lem1  47095  fnresfnco  47501  funcoressn  47502  fnfocofob  47539  fnbrafvb  47614  tz6.12-afv  47633  afvco2  47636  tz6.12-afv2  47700  fnbrafv2b  47708  imaelsetpreimafv  47867  imasetpreimafvbijlemfv  47874  imasetpreimafvbijlemfo  47877  plusfreseq  48652  ackvalsuc0val  49175