Theorem fnfun 6193

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

Syntax hints:   → wi 4   = wceq 1637  dom cdm 5305  Fun wfun 6089   Fn wfn 6090

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 198  df-an 385  df-fn 6098

This theorem is referenced by:  fnrel  6194  funfni  6196  fnco  6204  fnssresb  6208  ffun  6253  f1fun  6312  f1ofun  6349  fnbrfvb  6450  fvelimab  6468  fvun1  6484  elpreima  6553  respreima  6560  fnsnr  6650  fnprb  6691  fntpb  6692  fconst3  6696  fnfvima  6715  fnunirn  6729  nvof1o  6754  f1eqcocnv  6774  fnexALT  7356  curry1  7497  curry2  7500  suppvalfn  7530  suppfnss  7548  suppfnssOLD  7549  fnsuppres  7551  wfrlem2  7644  wfrlem14  7658  tfrlem4  7705  tfrlem5  7706  tfrlem11  7714  tz7.48-2  7767  tz7.49  7770  fndmeng  8264  fnfi  8471  fodomfi  8472  resfnfinfin  8479  fczfsuppd  8526  marypha2lem4  8577  inf0  8759  r1elss  8910  dfac8alem  9129  alephfp  9208  dfac3  9221  dfac9  9237  dfac12lem1  9244  dfac12lem2  9245  r1om  9345  cfsmolem  9371  alephsing  9377  zorn2lem1  9597  zorn2lem5  9601  zorn2lem6  9602  zorn2lem7  9603  ttukeylem3  9612  ttukeylem6  9615  fnct  9638  smobeth  9687  fpwwe2lem9  9739  wunr1om  9820  tskr1om  9868  tskr1om2  9869  uzrdg0i  12976  uzrdgsuci  12977  hashkf  13333  cshimadifsn  13793  cshimadifsn0  13794  shftfn  14030  phimullem  15695  imasaddvallem  16388  imasvscaval  16397  frmdss2  17599  lcomfsupp  19101  lidlval  19395  rspval  19396  psrbagev1  19712  psgnghm  20127  frlmsslsp  20339  iscldtop  21107  2ndcomap  21469  qtoptop  21711  basqtop  21722  qtoprest  21728  kqfvima  21741  isr0  21748  kqreglem1  21752  kqnrmlem1  21754  kqnrmlem2  21755  elrnust  22235  ustbas  22238  uniiccdif  23553  fcoinver  29737  mdetpmtr1  30208  fimaproj  30219  sseqf  30773  sseqfv2  30775  elorrvc  30844  bnj930  31157  bnj1371  31414  bnj1497  31445  frrlem2  32096  noextendseq  32135  madeval  32250  filnetlem4  32691  heibor1lem  33913  diaf11N  36824  dibf11N  36936  dibclN  36937  dihintcl  37119  ismrc  37760  dnnumch1  38109  aomclem4  38122  aomclem6  38124  ntrclsfv1  38847  ntrneifv1  38871  fvelimad  39936  fnfvimad  39937  fvelima2  39952  climrescn  40454  icccncfext  40574  stoweidlem29  40719  stoweidlem59  40749  ovolval4lem1  41339  fnresfnco  41654  funcoressn  41655  fnbrafvb  41737  tz6.12-afv  41756  afvco2  41759  tz6.12-afv2  41823  fnbrafv2b  41831  plusfreseq  42334  dfrngc2  42534  dfringc2  42580  rngcresringcat  42592  mndpsuppss  42714  mndpfsupp  42719