Theorem fnfun 6618

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5638  Fun wfun 6505   Fn wfn 6506

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 6514

This theorem is referenced by:  fnfund  6619  fnrel  6620  funfni  6624  fncofn  6635  fnco  6636  fnssresb  6640  ffun  6691  f1fun  6758  f1ofun  6802  fnbrfvb  6911  fvelima2  6913  fvelimad  6928  fvelimab  6933  fvun1  6952  elpreima  7030  respreima  7038  rescnvimafod  7045  fnsnr  7137  fnsnbg  7138  fnprb  7182  fntpb  7183  fconst3  7187  fnfvima  7207  ralima  7211  fnunirn  7228  nvof1o  7255  f1eqcocnv  7276  offun  7667  fnexALT  7929  curry1  8083  curry2  8086  fimaproj  8114  suppvalfng  8146  suppvalfn  8147  suppfnss  8168  fnsuppres  8170  frrlem2  8266  frrlem12  8276  tfrlem4  8347  tfrlem5  8348  tfrlem11  8356  tz7.48-2  8410  tz7.49  8413  naddcllem  8640  naddov2  8643  naddunif  8657  naddasslem1  8658  naddasslem2  8659  fndmeng  9006  fnfi  9142  fodomfi  9261  fodomfiOLD  9281  resfnfinfin  9288  finnzfsuppd  9324  fczfsuppd  9337  marypha2lem4  9389  inf0  9574  r1elss  9759  dfac8alem  9982  alephfp  10061  dfac3  10074  dfac9  10090  dfac12lem1  10097  dfac12lem2  10098  r1om  10196  cfsmolem  10223  alephsing  10229  zorn2lem1  10449  zorn2lem5  10453  zorn2lem6  10454  zorn2lem7  10455  ttukeylem3  10464  ttukeylem6  10467  fnct  10490  smobeth  10539  fpwwe2lem8  10591  wunr1om  10672  tskr1om  10720  tskr1om2  10721  uzrdg0i  13924  uzrdgsuci  13925  seqexw  13982  hashkf  14297  cshimadifsn  14795  cshimadifsn0  14796  shftfn  15039  phimullem  16749  imasaddvallem  17492  imasvscaval  17501  dfrngc2  20537  dfringc2  20566  rngcresringcat  20578  lidlval  21120  rspval  21121  psgnghm  21489  iscldtop  22982  2ndcomap  23345  qtoptop  23587  basqtop  23598  qtoprest  23604  kqfvima  23617  isr0  23624  kqreglem1  23628  kqnrmlem1  23630  kqnrmlem2  23631  ustbas  24115  uniiccdif  25479  noextendseq  27579  madeval  27760  oldval  27762  addsval  27869  negsval  27931  negsproplem2  27935  negsunif  27961  mulsval  28012  zsex  28268  fcoinver  32533  fnpreimac  32595  elrgspnlem2  33194  mdetpmtr1  33813  sseqf  34383  sseqfv2  34385  elorrvc  34455  bnj1371  35019  bnj1497  35050  fnrelpredd  35079  gblacfnacd  35089  onvf1odlem3  35092  onvf1odlem4  35093  onvf1od  35094  filnetlem4  36369  heibor1lem  37803  diaf11N  41043  dibf11N  41155  dibclN  41156  dihintcl  41338  aks6d1c2lem4  42115  ismrc  42689  dnnumch1  43033  aomclem4  43046  aomclem6  43048  tfsconcatrev  43337  tfsnfin  43341  fnimafnex  43429  ntrclsfv1  44044  ntrneifv1  44068  climrescn  45746  icccncfext  45885  stoweidlem29  46027  stoweidlem59  46057  ovolval4lem1  46647  fnresfnco  47042  funcoressn  47043  fnfocofob  47080  fnbrafvb  47155  tz6.12-afv  47174  afvco2  47177  tz6.12-afv2  47241  fnbrafv2b  47249  imaelsetpreimafv  47396  imasetpreimafvbijlemfv  47403  imasetpreimafvbijlemfo  47406  plusfreseq  48152  ackvalsuc0val  48676