Theorem fnfun 5988

Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fnfun	|- ( F Fn A -> Fun F )

Proof of Theorem fnfun

Step	Hyp	Ref	Expression
1		df-fn 5891	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simplbi 476	1 |- ( F Fn A -> Fun F )

Syntax hints:   -> wi 4   = wceq 1483   dom cdm 5114   Fun wfun 5882   Fn wfn 5883

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 197  df-an 386  df-fn 5891

This theorem is referenced by:  fnrel  5989  funfni  5991  fnco  5999  fnssresb  6003  ffun  6048  f1fun  6103  f1ofun  6139  fnbrfvb  6236  fvelimab  6253  fvun1  6269  elpreima  6337  respreima  6344  fnsnb  6432  fnprb  6472  fntpb  6473  fconst3  6477  fnfvima  6496  fnunirn  6511  nvof1o  6536  f1eqcocnv  6556  fnexALT  7132  curry1  7269  curry2  7272  suppvalfn  7302  suppfnss  7320  fnsuppres  7322  wfrlem2  7415  wfrlem14  7428  tfrlem4  7475  tfrlem5  7476  tfrlem11  7484  tz7.48-2  7537  tz7.49  7540  fndmeng  8034  fnfi  8238  fodomfi  8239  resfnfinfin  8246  fczfsuppd  8293  marypha2lem4  8344  inf0  8518  r1elss  8669  dfac8alem  8852  alephfp  8931  dfac3  8944  dfac9  8958  dfac12lem1  8965  dfac12lem2  8966  r1om  9066  cfsmolem  9092  alephsing  9098  zorn2lem1  9318  zorn2lem5  9322  zorn2lem6  9323  zorn2lem7  9324  ttukeylem3  9333  ttukeylem6  9336  fnct  9359  smobeth  9408  fpwwe2lem9  9460  wunr1om  9541  tskr1om  9589  tskr1om2  9590  uzrdg0i  12758  uzrdgsuci  12759  hashkf  13119  cshimadifsn  13575  cshimadifsn0  13576  shftfn  13813  phimullem  15484  imasaddvallem  16189  imasvscaval  16198  frmdss2  17400  lcomfsupp  18903  lidlval  19192  rspval  19193  psrbagev1  19510  psgnghm  19926  frlmsslsp  20135  iscldtop  20899  2ndcomap  21261  qtoptop  21503  basqtop  21514  qtoprest  21520  kqfvima  21533  isr0  21540  kqreglem1  21544  kqnrmlem1  21546  kqnrmlem2  21547  elrnust  22028  ustbas  22031  uniiccdif  23346  fcoinver  29418  mdetpmtr1  29889  fimaproj  29900  sseqf  30454  sseqfv2  30456  elorrvc  30525  bnj142OLD  30794  bnj930  30840  bnj1371  31097  bnj1497  31128  frrlem2  31781  noextendseq  31820  madeval  31935  filnetlem4  32376  heibor1lem  33608  diaf11N  36338  dibf11N  36450  dibclN  36451  dihintcl  36633  ismrc  37264  dnnumch1  37614  aomclem4  37627  aomclem6  37629  ntrclsfv1  38353  ntrneifv1  38377  fvelimad  39458  fnfvimad  39459  fvelima2  39475  climrescn  39980  icccncfext  40100  stoweidlem29  40246  stoweidlem59  40276  ovolval4lem1  40863  fnresfnco  41206  funcoressn  41207  fnbrafvb  41234  tz6.12-afv  41253  afvco2  41256  plusfreseq  41772  dfrngc2  41972  dfringc2  42018  rngcresringcat  42030  mndpsuppss  42152  mndpfsupp  42157