Theorem fnfun 5956

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

Syntax hints:   → wi 4   = wceq 1480  dom cdm 5084  Fun wfun 5851   Fn wfn 5852

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 197  df-an 386  df-fn 5860

This theorem is referenced by:  fnrel  5957  funfni  5959  fnco  5967  fnssresb  5971  ffun  6015  f1fun  6070  f1ofun  6106  fnbrfvb  6203  fvelimab  6220  fvun1  6236  elpreima  6303  respreima  6310  fnsnb  6397  fnprb  6437  fntpb  6438  fconst3  6442  fnfvima  6461  fnunirn  6476  nvof1o  6501  f1eqcocnv  6521  fnexALT  7094  curry1  7229  curry2  7232  suppvalfn  7262  suppfnss  7280  fnsuppres  7282  wfrlem2  7375  wfrlem14  7388  tfrlem4  7435  tfrlem5  7436  tfrlem11  7444  tz7.48-2  7497  tz7.49  7500  fndmeng  7994  fnfi  8198  fodomfi  8199  resfnfinfin  8206  fczfsuppd  8253  marypha2lem4  8304  inf0  8478  r1elss  8629  dfac8alem  8812  alephfp  8891  dfac3  8904  dfac9  8918  dfac12lem1  8925  dfac12lem2  8926  r1om  9026  cfsmolem  9052  alephsing  9058  zorn2lem1  9278  zorn2lem5  9282  zorn2lem6  9283  zorn2lem7  9284  ttukeylem3  9293  ttukeylem6  9296  fnct  9319  smobeth  9368  fpwwe2lem9  9420  wunr1om  9501  tskr1om  9549  tskr1om2  9550  uzrdg0i  12714  uzrdgsuci  12715  hashkf  13075  cshimadifsn  13528  cshimadifsn0  13529  shftfn  13763  phimullem  15427  imasaddvallem  16129  imasvscaval  16138  frmdss2  17340  lcomfsupp  18843  lidlval  19132  rspval  19133  psrbagev1  19450  psgnghm  19866  frlmsslsp  20075  iscldtop  20839  2ndcomap  21201  qtoptop  21443  basqtop  21454  qtoprest  21460  kqfvima  21473  isr0  21480  kqreglem1  21484  kqnrmlem1  21486  kqnrmlem2  21487  elrnust  21968  ustbas  21971  uniiccdif  23286  fcoinver  29302  mdetpmtr1  29713  fimaproj  29724  sseqf  30277  sseqfv2  30279  elorrvc  30348  bnj142OLD  30555  bnj930  30601  bnj1371  30858  bnj1497  30889  frrlem2  31535  filnetlem4  32071  heibor1lem  33279  diaf11N  35857  dibf11N  35969  dibclN  35970  dihintcl  36152  ismrc  36783  dnnumch1  37133  aomclem4  37146  aomclem6  37148  ntrclsfv1  37874  ntrneifv1  37898  fvelimad  38968  fnfvimad  38969  icccncfext  39435  stoweidlem29  39583  stoweidlem59  39613  ovolval4lem1  40200  fnresfnco  40540  funcoressn  40541  fnbrafvb  40568  tz6.12-afv  40587  afvco2  40590  plusfreseq  41090  dfrngc2  41290  dfringc2  41336  rngcresringcat  41348  mndpsuppss  41470  mndpfsupp  41475