Theorem fnfun 5678

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

Syntax hints:   -> wi 4   = wceq 1379   dom cdm 4999   Fun wfun 5582   Fn wfn 5583

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 185  df-an 371  df-fn 5591

This theorem is referenced by:  fnrel  5679  funfni  5681  fnco  5689  fnssresb  5693  ffun  5733  f1fun  5783  f1ofun  5818  fnbrfvb  5908  fvelimab  5923  fvun1  5938  elpreima  6001  respreima  6010  fnsnb  6080  fnprb  6119  fnprOLD  6120  fconst3  6124  fnfvima  6138  fnunirn  6153  nvof1o  6174  f1eqcocnv  6192  fnexALT  6750  curry1  6875  curry2  6878  suppvalfn  6908  suppfnss  6925  fnsuppres  6927  tfrlem4  7048  tfrlem5  7049  tfrlem11  7057  tz7.48-2  7107  tz7.49  7110  fndmeng  7592  fnfi  7798  fodomfi  7799  fczfsuppd  7847  marypha2lem4  7898  inf0  8038  noinfepOLD  8077  r1elss  8224  dfac8alem  8410  alephfp  8489  dfac3  8502  dfac9  8516  dfac12lem1  8523  dfac12lem2  8524  r1om  8624  cfsmolem  8650  alephsing  8656  zorn2lem1  8876  zorn2lem5  8880  zorn2lem6  8881  zorn2lem7  8882  ttukeylem3  8891  ttukeylem6  8894  smobeth  8961  fpwwe2lem9  9016  wunr1om  9097  tskr1om  9145  tskr1om2  9146  uzrdg0i  12038  uzrdgsuci  12039  hashkf  12375  shftfn  12869  phimullem  14168  imasaddvallem  14784  imasvscaval  14793  frmdss2  15863  dprdvalOLD  16839  lcomfsupp  17350  lidlval  17638  rspval  17639  psrbagev1  17976  psgnghm  18411  frlmsslsp  18624  frlmsslspOLD  18625  iscldtop  19390  2ndcomap  19753  qtoptop  19964  basqtop  19975  qtoprest  19981  kqfvima  19994  isr0  20001  kqreglem1  20005  kqnrmlem1  20007  kqnrmlem2  20008  elrnust  20490  ustbas  20493  uniiccdif  21750  eupap1  24680  fcoinver  27161  fnct  27236  fimaproj  27527  sseqf  27999  sseqfv2  28001  elorrvc  28070  wfrlem2  28949  wfrlem14  28961  frrlem2  28993  bpolylem  29415  filnetlem4  29830  heibor1lem  29936  ismrc  30265  dnnumch1  30622  aomclem4  30635  aomclem6  30637  icccncfext  31254  stoweidlem29  31357  stoweidlem59  31387  fnresfnco  31706  funcoressn  31707  fnbrafvb  31734  tz6.12-afv  31753  afvco2  31756  resfnfinfin  31805  mndpsuppss  32063  mndpfsupp  32068  bnj142OLD  32879  bnj930  32925  bnj1371  33182  bnj1497  33213  diaf11N  35864  dibf11N  35976  dibclN  35977  dihintcl  36159