Theorem fnfun 5503

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

Syntax hints:   -> wi 4   = wceq 1369   dom cdm 4835   Fun wfun 5407   Fn wfn 5408

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 5416

This theorem is referenced by:  fnrel  5504  funfni  5506  fnco  5514  fnssresb  5518  ffun  5556  f1fun  5603  f1ofun  5638  fnbrfvb  5727  fvelimab  5742  fvun1  5757  elpreima  5818  respreima  5827  fnsnb  5893  fnprb  5931  fnprOLD  5932  fconst3  5936  fnfvima  5950  fnunirn  5965  nvof1o  5982  f1eqcocnv  5994  fnexALT  6538  curry1  6659  curry2  6662  suppvalfn  6692  suppfnss  6709  fnsuppres  6711  tfrlem4  6830  tfrlem5  6831  tfrlem11  6839  tz7.48-2  6889  tz7.49  6892  fndmeng  7378  fnfi  7581  fodomfi  7582  fczfsuppd  7630  marypha2lem4  7680  inf0  7819  noinfepOLD  7858  r1elss  8005  dfac8alem  8191  alephfp  8270  dfac3  8283  dfac9  8297  dfac12lem1  8304  dfac12lem2  8305  r1om  8405  cfsmolem  8431  alephsing  8437  zorn2lem1  8657  zorn2lem5  8661  zorn2lem6  8662  zorn2lem7  8663  ttukeylem3  8672  ttukeylem6  8675  smobeth  8742  fpwwe2lem9  8797  wunr1om  8878  tskr1om  8926  tskr1om2  8927  uzrdg0i  11774  uzrdgsuci  11775  hashkf  12097  shftfn  12554  phimullem  13846  imasaddvallem  14459  imasvscaval  14468  frmdss2  15532  dprdvalOLD  16475  lcomfsupp  16963  lidlval  17250  rspval  17251  psrbagev1  17569  psgnghm  17985  frlmsslsp  18198  frlmsslspOLD  18199  iscldtop  18674  2ndcomap  19037  qtoptop  19248  basqtop  19259  qtoprest  19265  kqfvima  19278  isr0  19285  kqreglem1  19289  kqnrmlem1  19291  kqnrmlem2  19292  elrnust  19774  ustbas  19777  uniiccdif  21033  eupap1  23548  fnct  25964  sseqf  26727  sseqfv2  26729  elorrvc  26798  wfrlem2  27676  wfrlem14  27688  frrlem2  27720  bpolylem  28142  filnetlem4  28555  heibor1lem  28661  ismrc  28990  dnnumch1  29350  aomclem4  29363  aomclem6  29365  stoweidlem29  29777  stoweidlem59  29807  fnresfnco  29985  funcoressn  29986  fnbrafvb  30013  tz6.12-afv  30032  afvco2  30035  resfnfinfin  30118  mndpsuppss  30735  mndpfsupp  30740  bnj142OLD  31604  bnj930  31650  bnj1371  31907  bnj1497  31938  diaf11N  34534  dibf11N  34646  dibclN  34647  dihintcl  34829