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 497	1 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Syntax hints:   → wi 4   = wceq 1541  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  7003  respreima  7011  rescnvimafod  7018  fnsnr  7109  fnsnbg  7110  fnprb  7154  fntpb  7155  fconst3  7159  fnfvima  7179  ralima  7183  fnunirn  7199  nvof1o  7226  f1eqcocnv  7247  offun  7636  fnexALT  7895  curry1  8046  curry2  8049  fimaproj  8077  suppvalfng  8109  suppvalfn  8110  suppfnss  8131  fnsuppres  8133  frrlem2  8229  frrlem12  8239  tfrlem4  8310  tfrlem5  8311  tfrlem11  8319  tz7.48-2  8373  tz7.49  8376  naddcllem  8604  naddov2  8607  naddunif  8621  naddasslem1  8622  naddasslem2  8623  fndmeng  8972  fnfi  9102  fodomfi  9212  fodomfiOLD  9230  resfnfinfin  9237  tfsnfin2  9263  finnzfsuppd  9276  fczfsuppd  9289  marypha2lem4  9341  inf0  9530  r1elss  9718  dfac8alem  9939  alephfp  10018  dfac3  10031  dfac9  10047  dfac12lem1  10054  dfac12lem2  10055  r1om  10153  cfsmolem  10180  alephsing  10186  zorn2lem1  10406  zorn2lem5  10410  zorn2lem6  10411  zorn2lem7  10412  ttukeylem3  10421  ttukeylem6  10424  fnct  10447  smobeth  10497  fpwwe2lem8  10549  wunr1om  10630  tskr1om  10678  tskr1om2  10679  uzrdg0i  13882  uzrdgsuci  13883  seqexw  13940  hashkf  14255  cshimadifsn  14752  cshimadifsn0  14753  shftfn  14996  phimullem  16706  imasaddvallem  17450  imasvscaval  17459  dfrngc2  20561  dfringc2  20590  rngcresringcat  20602  lidlval  21165  rspval  21166  psgnghm  21535  iscldtop  23039  2ndcomap  23402  qtoptop  23644  basqtop  23655  qtoprest  23661  kqfvima  23674  isr0  23681  kqreglem1  23685  kqnrmlem1  23687  kqnrmlem2  23688  ustbas  24171  uniiccdif  25535  noextendseq  27635  madeval  27828  oldval  27830  addsval  27958  negsval  28021  negsproplem2  28025  negsunif  28051  mulsval  28105  zsex  28376  fcoinver  32679  fresunsn  32703  fnpreimac  32749  elrgspnlem2  33325  mdetpmtr1  33980  sseqf  34549  sseqfv2  34551  elorrvc  34621  bnj1371  35185  bnj1497  35216  fnrelpredd  35247  gblacfnacd  35296  onvf1odlem3  35299  onvf1odlem4  35300  onvf1od  35301  filnetlem4  36575  heibor1lem  38006  diaf11N  41305  dibf11N  41417  dibclN  41418  dihintcl  41600  aks6d1c2lem4  42377  ismrc  42939  dnnumch1  43282  aomclem4  43295  aomclem6  43297  tfsconcatrev  43586  tfsnfin  43590  fnimafnex  43677  ntrclsfv1  44292  ntrneifv1  44316  climrescn  45988  icccncfext  46127  stoweidlem29  46269  stoweidlem59  46299  ovolval4lem1  46889  fnresfnco  47283  funcoressn  47284  fnfocofob  47321  fnbrafvb  47396  tz6.12-afv  47415  afvco2  47418  tz6.12-afv2  47482  fnbrafv2b  47490  imaelsetpreimafv  47637  imasetpreimafvbijlemfv  47644  imasetpreimafvbijlemfo  47647  plusfreseq  48406  ackvalsuc0val  48929