Theorem fnfun 6542

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5590  Fun wfun 6431   Fn wfn 6432

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 206  df-an 397  df-fn 6440

This theorem is referenced by:  fnfund  6543  fnrel  6544  funfni  6548  fncofn  6557  fnco  6558  fncoOLD  6559  fnssresb  6563  ffun  6612  f1fun  6681  f1ofun  6727  fnbrfvb  6831  fvelimad  6845  fvelimab  6850  fvun1  6868  elpreima  6944  respreima  6952  rescnvimafod  6960  fnsnr  7046  fnprb  7093  fntpb  7094  fconst3  7098  fnfvima  7118  fnunirn  7136  nvof1o  7161  f1eqcocnv  7182  f1eqcocnvOLD  7183  offun  7556  fnexALT  7802  curry1  7953  curry2  7956  fimaproj  7985  suppvalfng  7993  suppvalfn  7994  suppfnss  8014  fnsuppres  8016  frrlem2  8112  frrlem12  8122  wfrlem2OLD  8149  wfrlem14OLD  8162  tfrlem4  8219  tfrlem5  8220  tfrlem11  8228  tz7.48-2  8282  tz7.49  8285  fndmeng  8834  fnfi  8973  fodomfi  9101  resfnfinfin  9108  fczfsuppd  9155  marypha2lem4  9206  inf0  9388  r1elss  9573  dfac8alem  9794  alephfp  9873  dfac3  9886  dfac9  9901  dfac12lem1  9908  dfac12lem2  9909  r1om  10009  cfsmolem  10035  alephsing  10041  zorn2lem1  10261  zorn2lem5  10265  zorn2lem6  10266  zorn2lem7  10267  ttukeylem3  10276  ttukeylem6  10279  fnct  10302  smobeth  10351  fpwwe2lem8  10403  wunr1om  10484  tskr1om  10532  tskr1om2  10533  uzrdg0i  13688  uzrdgsuci  13689  seqexw  13746  hashkf  14055  cshimadifsn  14551  cshimadifsn0  14552  shftfn  14793  phimullem  16489  imasaddvallem  17249  imasvscaval  17258  lidlval  20471  rspval  20472  psgnghm  20794  iscldtop  22255  2ndcomap  22618  qtoptop  22860  basqtop  22871  qtoprest  22877  kqfvima  22890  isr0  22897  kqreglem1  22901  kqnrmlem1  22903  kqnrmlem2  22904  elrnust  23385  ustbas  23388  uniiccdif  24751  fcoinver  30955  fnpreimac  31017  mdetpmtr1  31782  sseqf  32368  sseqfv2  32370  elorrvc  32439  bnj1371  33018  bnj1497  33049  fnrelpredd  33070  naddcllem  33840  naddov2  33843  noextendseq  33879  madeval  34045  oldval  34047  negsval  34132  addsval  34135  filnetlem4  34579  heibor1lem  35976  diaf11N  39070  dibf11N  39182  dibclN  39183  dihintcl  39365  fnsnbt  40215  ismrc  40530  dnnumch1  40876  aomclem4  40889  aomclem6  40891  ntrclsfv1  41672  ntrneifv1  41696  finnzfsuppd  41827  fvelima2  42813  climrescn  43296  icccncfext  43435  stoweidlem29  43577  stoweidlem59  43607  ovolval4lem1  44194  fnresfnco  44546  funcoressn  44547  fnfocofob  44582  fnbrafvb  44657  tz6.12-afv  44676  afvco2  44679  tz6.12-afv2  44743  fnbrafv2b  44751  imaelsetpreimafv  44858  imasetpreimafvbijlemfv  44865  imasetpreimafvbijlemfo  44868  plusfreseq  45337  dfrngc2  45541  dfringc2  45587  rngcresringcat  45599  ackvalsuc0val  46044