Theorem fnfun 6586

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5619  Fun wfun 6480   Fn wfn 6481

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 6489

This theorem is referenced by:  fnfund  6587  fnrel  6588  funfni  6592  fncofn  6603  fnco  6604  fnssresb  6608  ffun  6659  f1fun  6726  f1ofun  6770  fnbrfvb  6878  fvelima2  6880  fvelimad  6895  fvelimab  6900  fvun1  6919  elpreima  6997  respreima  7005  rescnvimafod  7012  fnsnr  7103  fnsnbg  7104  fnprb  7148  fntpb  7149  fconst3  7153  fnfvima  7173  ralima  7177  fnunirn  7193  nvof1o  7220  f1eqcocnv  7241  offun  7630  fnexALT  7889  curry1  8040  curry2  8043  fimaproj  8071  suppvalfng  8103  suppvalfn  8104  suppfnss  8125  fnsuppres  8127  frrlem2  8223  frrlem12  8233  tfrlem4  8304  tfrlem5  8305  tfrlem11  8313  tz7.48-2  8367  tz7.49  8370  naddcllem  8597  naddov2  8600  naddunif  8614  naddasslem1  8615  naddasslem2  8616  fndmeng  8964  fnfi  9094  fodomfi  9203  fodomfiOLD  9221  resfnfinfin  9228  finnzfsuppd  9264  fczfsuppd  9277  marypha2lem4  9329  inf0  9518  r1elss  9706  dfac8alem  9927  alephfp  10006  dfac3  10019  dfac9  10035  dfac12lem1  10042  dfac12lem2  10043  r1om  10141  cfsmolem  10168  alephsing  10174  zorn2lem1  10394  zorn2lem5  10398  zorn2lem6  10399  zorn2lem7  10400  ttukeylem3  10409  ttukeylem6  10412  fnct  10435  smobeth  10484  fpwwe2lem8  10536  wunr1om  10617  tskr1om  10665  tskr1om2  10666  uzrdg0i  13868  uzrdgsuci  13869  seqexw  13926  hashkf  14241  cshimadifsn  14738  cshimadifsn0  14739  shftfn  14982  phimullem  16692  imasaddvallem  17435  imasvscaval  17444  dfrngc2  20545  dfringc2  20574  rngcresringcat  20586  lidlval  21149  rspval  21150  psgnghm  21519  iscldtop  23011  2ndcomap  23374  qtoptop  23616  basqtop  23627  qtoprest  23633  kqfvima  23646  isr0  23653  kqreglem1  23657  kqnrmlem1  23659  kqnrmlem2  23660  ustbas  24143  uniiccdif  25507  noextendseq  27607  madeval  27794  oldval  27796  addsval  27906  negsval  27968  negsproplem2  27972  negsunif  27998  mulsval  28049  zsex  28305  fcoinver  32586  fnpreimac  32655  elrgspnlem2  33217  mdetpmtr1  33857  sseqf  34426  sseqfv2  34428  elorrvc  34498  bnj1371  35062  bnj1497  35093  fnrelpredd  35123  gblacfnacd  35167  onvf1odlem3  35170  onvf1odlem4  35171  onvf1od  35172  filnetlem4  36446  heibor1lem  37870  diaf11N  41169  dibf11N  41281  dibclN  41282  dihintcl  41464  aks6d1c2lem4  42241  ismrc  42819  dnnumch1  43162  aomclem4  43175  aomclem6  43177  tfsconcatrev  43466  tfsnfin  43470  fnimafnex  43558  ntrclsfv1  44173  ntrneifv1  44197  climrescn  45871  icccncfext  46010  stoweidlem29  46152  stoweidlem59  46182  ovolval4lem1  46772  fnresfnco  47166  funcoressn  47167  fnfocofob  47204  fnbrafvb  47279  tz6.12-afv  47298  afvco2  47301  tz6.12-afv2  47365  fnbrafv2b  47373  imaelsetpreimafv  47520  imasetpreimafvbijlemfv  47527  imasetpreimafvbijlemfo  47530  plusfreseq  48289  ackvalsuc0val  48813