Theorem fnfun 5688

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 5601	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simplbi 461	1 |- ( F Fn A -> Fun F )

Syntax hints:   -> wi 4   = wceq 1437   dom cdm 4850   Fun wfun 5592   Fn wfn 5593

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 188  df-an 372  df-fn 5601

This theorem is referenced by:  fnrel  5689  funfni  5691  fnco  5699  fnssresb  5703  ffun  5745  f1fun  5795  f1ofun  5830  fnbrfvb  5918  fvelimab  5934  fvun1  5949  elpreima  6014  respreima  6021  fnsnb  6095  fnprb  6135  fconst3  6140  fnfvima  6155  fnunirn  6170  nvof1o  6191  f1eqcocnv  6211  fnexALT  6770  curry1  6896  curry2  6899  suppvalfn  6929  suppfnss  6948  fnsuppres  6950  wfrlem2  7041  wfrlem14  7054  tfrlem4  7102  tfrlem5  7103  tfrlem11  7111  tz7.48-2  7164  tz7.49  7167  fndmeng  7650  fnfi  7852  fodomfi  7853  fczfsuppd  7904  marypha2lem4  7955  inf0  8129  r1elss  8279  dfac8alem  8461  alephfp  8540  dfac3  8553  dfac9  8567  dfac12lem1  8574  dfac12lem2  8575  r1om  8675  cfsmolem  8701  alephsing  8707  zorn2lem1  8927  zorn2lem5  8931  zorn2lem6  8932  zorn2lem7  8933  ttukeylem3  8942  ttukeylem6  8945  smobeth  9012  fpwwe2lem9  9064  wunr1om  9145  tskr1om  9193  tskr1om2  9194  uzrdg0i  12173  uzrdgsuci  12174  hashkf  12517  shftfn  13125  phimullem  14715  imasaddvallem  15423  imasvscaval  15432  frmdss2  16635  lcomfsupp  18116  lidlval  18403  rspval  18404  psrbagev1  18721  psgnghm  19135  frlmsslsp  19341  iscldtop  20098  2ndcomap  20460  qtoptop  20702  basqtop  20713  qtoprest  20719  kqfvima  20732  isr0  20739  kqreglem1  20743  kqnrmlem1  20745  kqnrmlem2  20746  elrnust  21226  ustbas  21229  uniiccdif  22522  eupap1  25690  fcoinver  28204  fnct  28291  mdetpmtr1  28645  fimaproj  28656  sseqf  29221  sseqfv2  29223  elorrvc  29292  bnj142OLD  29530  bnj930  29577  bnj1371  29834  bnj1497  29865  frrlem2  30510  filnetlem4  31030  heibor1lem  32055  diaf11N  34536  dibf11N  34648  dibclN  34649  dihintcl  34831  ismrc  35462  dnnumch1  35822  aomclem4  35835  aomclem6  35837  icccncfext  37585  stoweidlem29  37709  stoweidlem29OLD  37710  stoweidlem59  37740  fnresfnco  38340  funcoressn  38341  fnbrafvb  38368  tz6.12-afv  38387  afvco2  38390  resfnfinfin  38727  plusfreseq  39044  dfrngc2  39246  dfringc2  39292  rngcresringcat  39304  mndpsuppss  39430  mndpfsupp  39435