Theorem fnfun 5902

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

Syntax hints:   → wi 4   = wceq 1475  dom cdm 5038  Fun wfun 5798   Fn wfn 5799

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 196  df-an 385  df-fn 5807

This theorem is referenced by:  fnrel  5903  funfni  5905  fnco  5913  fnssresb  5917  ffun  5961  f1fun  6016  f1ofun  6052  fnbrfvb  6146  fvelimab  6163  fvun1  6179  elpreima  6245  respreima  6252  fnsnb  6337  fnprb  6377  fntpb  6378  fconst3  6382  fnfvima  6400  fnunirn  6415  nvof1o  6436  f1eqcocnv  6456  fnexALT  7025  curry1  7156  curry2  7159  suppvalfn  7189  suppfnss  7207  fnsuppres  7209  wfrlem2  7302  wfrlem14  7315  tfrlem4  7362  tfrlem5  7363  tfrlem11  7371  tz7.48-2  7424  tz7.49  7427  fndmeng  7919  fnfi  8123  fodomfi  8124  fczfsuppd  8176  marypha2lem4  8227  inf0  8401  r1elss  8552  dfac8alem  8735  alephfp  8814  dfac3  8827  dfac9  8841  dfac12lem1  8848  dfac12lem2  8849  r1om  8949  cfsmolem  8975  alephsing  8981  zorn2lem1  9201  zorn2lem5  9205  zorn2lem6  9206  zorn2lem7  9207  ttukeylem3  9216  ttukeylem6  9219  smobeth  9287  fpwwe2lem9  9339  wunr1om  9420  tskr1om  9468  tskr1om2  9469  uzrdg0i  12620  uzrdgsuci  12621  hashkf  12981  cshimadifsn  13426  cshimadifsn0  13427  shftfn  13661  phimullem  15322  imasaddvallem  16012  imasvscaval  16021  frmdss2  17223  lcomfsupp  18726  lidlval  19013  rspval  19014  psrbagev1  19331  psgnghm  19745  frlmsslsp  19954  iscldtop  20709  2ndcomap  21071  qtoptop  21313  basqtop  21324  qtoprest  21330  kqfvima  21343  isr0  21350  kqreglem1  21354  kqnrmlem1  21356  kqnrmlem2  21357  elrnust  21838  ustbas  21841  uniiccdif  23152  eupap1  26503  fcoinver  28798  fnct  28876  mdetpmtr1  29217  fimaproj  29228  sseqf  29781  sseqfv2  29783  elorrvc  29852  bnj142OLD  30048  bnj930  30094  bnj1371  30351  bnj1497  30382  frrlem2  31025  filnetlem4  31546  heibor1lem  32778  diaf11N  35356  dibf11N  35468  dibclN  35469  dihintcl  35651  ismrc  36282  dnnumch1  36632  aomclem4  36645  aomclem6  36647  ntrclsfv1  37373  ntrneifv1  37397  icccncfext  38773  stoweidlem29  38922  stoweidlem59  38952  ovolval4lem1  39539  fnresfnco  39855  funcoressn  39856  fnbrafvb  39883  tz6.12-afv  39902  afvco2  39905  resfnfinfin  40339  plusfreseq  41562  dfrngc2  41764  dfringc2  41810  rngcresringcat  41822  mndpsuppss  41946  mndpfsupp  41951