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 1547  dom cdm 5625  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 208  df-an 397  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  7006  respreima  7014  rescnvimafod  7021  fnsnr  7114  fnsnbg  7115  fnprb  7159  fntpb  7160  fconst3  7164  fnfvima  7184  ralima  7188  fnunirn  7204  nvof1o  7231  f1eqcocnv  7252  offun  7641  fnexALT  7900  curry1  8050  curry2  8053  fimaproj  8082  suppvalfng  8114  suppvalfn  8115  suppfnss  8136  fnsuppres  8138  frrlem2  8234  frrlem12  8244  tfrlem4  8315  tfrlem5  8316  tfrlem11  8324  tz7.48-2  8378  tz7.49  8381  naddcllem  8609  naddov2  8612  naddunif  8626  naddasslem1  8627  naddasslem2  8628  fndmeng  8979  fnfi  9109  fodomfi  9219  fodomfiOLD  9237  resfnfinfin  9244  tfsnfin2  9270  finnzfsuppd  9283  fczfsuppd  9296  marypha2lem4  9348  inf0  9540  r1elss  9728  dfac8alem  9949  alephfp  10028  dfac3  10041  dfac9  10057  dfac12lem1  10064  dfac12lem2  10065  r1om  10163  cfsmolem  10190  alephsing  10196  zorn2lem1  10416  zorn2lem5  10420  zorn2lem6  10421  zorn2lem7  10422  ttukeylem3  10431  ttukeylem6  10434  fnct  10457  smobeth  10507  fpwwe2lem8  10559  wunr1om  10640  tskr1om  10688  tskr1om2  10689  uzrdg0i  13919  uzrdgsuci  13920  seqexw  13977  hashkf  14292  cshimadifsn  14789  cshimadifsn0  14790  shftfn  15033  phimullem  16747  imasaddvallem  17491  imasvscaval  17500  dfrngc2  20607  dfringc2  20636  rngcresringcat  20648  lidlval  21210  rspval  21211  psgnghm  21562  iscldtop  23085  2ndcomap  23448  qtoptop  23690  basqtop  23701  qtoprest  23707  kqfvima  23720  isr0  23727  kqreglem1  23731  kqnrmlem1  23733  kqnrmlem2  23734  ustbas  24217  uniiccdif  25570  noextendseq  27656  madeval  27849  oldval  27851  addsval  27979  negsval  28042  negsproplem2  28046  negsunif  28072  mulsval  28126  zsex  28397  nowisdomv  30569  fcoinver  32700  fresunsn  32724  fnpreimac  32769  elrgspnlem2  33331  mdetpmtr1  34014  sseqf  34583  sseqfv2  34585  elorrvc  34655  bnj1371  35218  bnj1497  35249  fnrelpredd  35279  gblacfnacd  35337  onvf1odlem3  35340  onvf1odlem4  35341  onvf1od  35342  filnetlem4  36616  heibor1lem  38183  diaf11N  41548  dibf11N  41660  dibclN  41661  dihintcl  41843  aks6d1c2lem4  42619  ismrc  43157  dnnumch1  43496  aomclem4  43509  aomclem6  43511  tfsconcatrev  43800  tfsnfin  43804  fnimafnex  43891  ntrclsfv1  44506  ntrneifv1  44530  climrescn  46198  icccncfext  46337  stoweidlem29  46479  stoweidlem59  46509  ovolval4lem1  47099  fnresfnco  47511  funcoressn  47512  fnfocofob  47549  fnbrafvb  47624  tz6.12-afv  47643  afvco2  47646  tz6.12-afv2  47710  fnbrafv2b  47718  imaelsetpreimafv  47877  imasetpreimafvbijlemfv  47884  imasetpreimafvbijlemfo  47887  plusfreseq  48662  ackvalsuc0val  49185