Theorem fnfun 6639

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  dom cdm 5650  Fun wfun 6532   Fn wfn 6533

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 6541

This theorem is used by:  fnfund  6640  fnrel  6641  funfni  6645  fncofn  6656  fnco  6657  fnssresb  6661  ffunOLD  6713  f1funOLD  6781  f1ofun  6826  fnbrfvb  6935  fvelima2  6937  fvelimad  6952  fvelimab  6957  fvun1  6976  elpreima  7057  respreima  7065  rescnvimafod  7073  fnsnr  7168  fnsnbg  7169  fnprb  7214  fntpb  7215  fconst3  7219  fnfvima  7239  ralima  7243  fnunirn  7257  nvof1o  7288  f1eqcocnv  7309  offun  7707  fnexALT  7963  curry1  8117  curry2  8120  fimaproj  8154  suppvalfng  8187  suppvalfn  8188  suppfnss  8209  fnsuppres  8211  frrlem2  8308  frrlem12  8318  tfrlem4  8389  tfrlem5  8390  tfrlem11  8399  tz7.48-2  8455  tz7.49  8458  naddcllem  8688  naddov2  8691  naddunif  8706  naddasslem1  8707  naddasslem2  8708  fndmeng  9066  fnfi  9196  fodomfi  9307  resfnfinfin  9329  tfsnfin2  9355  finnzfsuppd  9368  fczfsuppd  9381  marypha2lem4  9433  inf0  9625  r1elss  9817  dfac8alem  10111  alephfp  10190  dfac3  10203  dfac9  10218  dfac12lem1  10225  dfac12lem2  10226  cfsmolem  10351  alephsing  10357  zorn2lem1  10577  zorn2lem5  10581  zorn2lem6  10582  zorn2lem7  10583  ttukeylem3  10592  ttukeylem6  10595  fnct  10623  fnctOLD  10624  smobeth  10674  fpwwe2lem8  10726  uzrdg0i  14105  uzrdgsuci  14106  seqexw  14163  hashkf  14479  cshimadifsn  14984  cshimadifsn0  14985  shftfn  15231  phimullem  16961  imasaddvallem  17706  imasvscaval  17715  dfrngc2  20885  dfringc2  20914  rngcresringcat  20926  lidlval  21493  rspval  21494  psgnghm  21891  iscldtop  23418  2ndcomap  23782  qtoptop  24024  basqtop  24035  qtoprest  24041  kqfvima  24054  isr0  24061  kqreglem1  24065  kqnrmlem1  24067  kqnrmlem2  24068  ustbas  24551  uniiccdif  25904  noextendseq  28029  madeval  28223  oldval  28225  addsval  28353  negsval  28416  negsproplem2  28420  negsunif  28446  mulsval  28500  zsex  28771  nowisdomv  31080  fcoinver  33245  fresunsn  33266  fnpreimac  33311  elrgspnlem2  33850  mdetpmtr1  34501  sseqf  35070  sseqfv2  35072  elorrvc  35142  bnj1371  35705  bnj1497  35736  fnrelpredd  35772  acwer1prc  35816  gblacfnacd  35948  onvf1odlem3  35952  onvf1odlem4  35953  onvf1od  35954  nmulprop  37031  filnetlem4  37261  heibor1lem  38836  diaf11N  42199  dibf11N  42311  dibclN  42312  dihintcl  42494  aks6d1c2lem4  43270  ismrc  43805  dnnumch1  44144  aomclem4  44152  aomclem6  44154  tfsconcatrev  44443  tfsnfin  44447  fnimafnex  44534  ntrclsfv1  45148  ntrneifv1  45172  climrescn  46851  icccncfext  46990  stoweidlem29  47132  stoweidlem59  47162  ovolval4lem1  47752  fnresfnco  48204  funcoressn  48205  fnfocofob  48242  fnbrafvb  48317  tz6.12-afv  48336  afvco2  48339  tz6.12-afv2  48403  fnbrafv2b  48411  imaelsetpreimafv  48570  imasetpreimafvbijlemfv  48577  imasetpreimafvbijlemfo  48580  plusfreseq  49354  ackvalsuc0val  49892