Theorem fnfun 6600

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5632  Fun wfun 6494   Fn wfn 6495

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 6503

This theorem is referenced by:  fnfund  6601  fnrel  6602  funfni  6606  fncofn  6617  fnco  6618  fnssresb  6622  ffun  6673  f1fun  6740  f1ofun  6784  fnbrfvb  6892  fvelima2  6894  fvelimad  6909  fvelimab  6914  fvun1  6933  elpreima  7012  respreima  7020  rescnvimafod  7027  fnsnr  7119  fnsnbg  7120  fnprb  7164  fntpb  7165  fconst3  7169  fnfvima  7189  ralima  7193  fnunirn  7209  nvof1o  7236  f1eqcocnv  7257  offun  7646  fnexALT  7905  curry1  8056  curry2  8059  fimaproj  8087  suppvalfng  8119  suppvalfn  8120  suppfnss  8141  fnsuppres  8143  frrlem2  8239  frrlem12  8249  tfrlem4  8320  tfrlem5  8321  tfrlem11  8329  tz7.48-2  8383  tz7.49  8386  naddcllem  8614  naddov2  8617  naddunif  8631  naddasslem1  8632  naddasslem2  8633  fndmeng  8984  fnfi  9114  fodomfi  9224  fodomfiOLD  9242  resfnfinfin  9249  tfsnfin2  9275  finnzfsuppd  9288  fczfsuppd  9301  marypha2lem4  9353  inf0  9542  r1elss  9730  dfac8alem  9951  alephfp  10030  dfac3  10043  dfac9  10059  dfac12lem1  10066  dfac12lem2  10067  r1om  10165  cfsmolem  10192  alephsing  10198  zorn2lem1  10418  zorn2lem5  10422  zorn2lem6  10423  zorn2lem7  10424  ttukeylem3  10433  ttukeylem6  10436  fnct  10459  smobeth  10509  fpwwe2lem8  10561  wunr1om  10642  tskr1om  10690  tskr1om2  10691  uzrdg0i  13894  uzrdgsuci  13895  seqexw  13952  hashkf  14267  cshimadifsn  14764  cshimadifsn0  14765  shftfn  15008  phimullem  16718  imasaddvallem  17462  imasvscaval  17471  dfrngc2  20573  dfringc2  20602  rngcresringcat  20614  lidlval  21177  rspval  21178  psgnghm  21547  iscldtop  23051  2ndcomap  23414  qtoptop  23656  basqtop  23667  qtoprest  23673  kqfvima  23686  isr0  23693  kqreglem1  23697  kqnrmlem1  23699  kqnrmlem2  23700  ustbas  24183  uniiccdif  25547  noextendseq  27647  madeval  27840  oldval  27842  addsval  27970  negsval  28033  negsproplem2  28037  negsunif  28063  mulsval  28117  zsex  28388  fcoinver  32690  fresunsn  32714  fnpreimac  32759  elrgspnlem2  33336  mdetpmtr1  34000  sseqf  34569  sseqfv2  34571  elorrvc  34641  bnj1371  35204  bnj1497  35235  fnrelpredd  35266  gblacfnacd  35315  onvf1odlem3  35318  onvf1odlem4  35319  onvf1od  35320  filnetlem4  36594  heibor1lem  38054  diaf11N  41419  dibf11N  41531  dibclN  41532  dihintcl  41714  aks6d1c2lem4  42491  ismrc  43052  dnnumch1  43395  aomclem4  43408  aomclem6  43410  tfsconcatrev  43699  tfsnfin  43703  fnimafnex  43790  ntrclsfv1  44405  ntrneifv1  44429  climrescn  46100  icccncfext  46239  stoweidlem29  46381  stoweidlem59  46411  ovolval4lem1  47001  fnresfnco  47395  funcoressn  47396  fnfocofob  47433  fnbrafvb  47508  tz6.12-afv  47527  afvco2  47530  tz6.12-afv2  47594  fnbrafv2b  47602  imaelsetpreimafv  47749  imasetpreimafvbijlemfv  47756  imasetpreimafvbijlemfo  47759  plusfreseq  48518  ackvalsuc0val  49041