Theorem fnfun 6631

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5651  Fun wfun 6525   Fn wfn 6526

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6534

This theorem is used by:  fnfund  6632  fnrel  6633  funfni  6637  fncofn  6648  fnco  6649  fnssresb  6653  ffunOLD  6705  f1funOLD  6773  f1ofun  6818  fnbrfvb  6927  fvelima2  6929  fvelimad  6944  fvelimab  6949  fvun1  6968  elpreima  7049  respreima  7057  rescnvimafod  7065  fnsnr  7160  fnsnbg  7161  fnprb  7206  fntpb  7207  fconst3  7211  fnfvima  7231  ralima  7235  fnunirn  7249  nvof1o  7280  f1eqcocnv  7301  offun  7696  fnexALT  7952  curry1  8104  curry2  8107  fimaproj  8136  suppvalfng  8168  suppvalfn  8169  suppfnss  8190  fnsuppres  8192  frrlem2  8289  frrlem12  8299  tfrlem4  8370  tfrlem5  8371  tfrlem11  8380  tz7.48-2  8436  tz7.49  8439  naddcllem  8669  naddov2  8672  naddunif  8687  naddasslem1  8688  naddasslem2  8689  fndmeng  9047  fnfi  9177  fodomfi  9288  resfnfinfin  9310  tfsnfin2  9336  finnzfsuppd  9349  fczfsuppd  9362  marypha2lem4  9414  inf0  9606  r1elss  9796  dfac8alem  10089  alephfp  10168  dfac3  10181  dfac9  10196  dfac12lem1  10203  dfac12lem2  10204  cfsmolem  10329  alephsing  10335  zorn2lem1  10555  zorn2lem5  10559  zorn2lem6  10560  zorn2lem7  10561  ttukeylem3  10570  ttukeylem6  10573  fnct  10601  fnctOLD  10602  smobeth  10652  fpwwe2lem8  10704  wunr1om  10785  tskr1om  10833  tskhf  10834  uzrdg0i  14082  uzrdgsuci  14083  seqexw  14140  hashkf  14456  cshimadifsn  14960  cshimadifsn0  14961  shftfn  15206  phimullem  16936  imasaddvallem  17681  imasvscaval  17690  dfrngc2  20860  dfringc2  20889  rngcresringcat  20901  lidlval  21468  rspval  21469  psgnghm  21866  iscldtop  23393  2ndcomap  23757  qtoptop  23999  basqtop  24010  qtoprest  24016  kqfvima  24029  isr0  24036  kqreglem1  24040  kqnrmlem1  24042  kqnrmlem2  24043  ustbas  24526  uniiccdif  25879  noextendseq  28006  madeval  28200  oldval  28202  addsval  28330  negsval  28393  negsproplem2  28397  negsunif  28423  mulsval  28477  zsex  28748  nowisdomv  31057  fcoinver  33180  fresunsn  33201  fnpreimac  33246  elrgspnlem2  33786  mdetpmtr1  34437  sseqf  35007  sseqfv2  35009  elorrvc  35079  bnj1371  35642  bnj1497  35673  fnrelpredd  35699  gblacfnacd  35854  onvf1odlem3  35857  onvf1odlem4  35858  onvf1od  35859  nmulprop  36909  filnetlem4  37139  heibor1lem  38711  diaf11N  42074  dibf11N  42186  dibclN  42187  dihintcl  42369  aks6d1c2lem4  43145  ismrc  43665  dnnumch1  44004  aomclem4  44017  aomclem6  44019  tfsconcatrev  44308  tfsnfin  44312  fnimafnex  44399  ntrclsfv1  45014  ntrneifv1  45038  climrescn  46702  icccncfext  46841  stoweidlem29  46983  stoweidlem59  47013  ovolval4lem1  47603  fnresfnco  48055  funcoressn  48056  fnfocofob  48093  fnbrafvb  48168  tz6.12-afv  48187  afvco2  48190  tz6.12-afv2  48254  fnbrafv2b  48262  imaelsetpreimafv  48421  imasetpreimafvbijlemfv  48428  imasetpreimafvbijlemfo  48431  plusfreseq  49205  ackvalsuc0val  49743