Theorem fnfun 6679

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

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5700  Fun wfun 6567   Fn wfn 6568

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 207  df-an 396  df-fn 6576

This theorem is referenced by:  fnfund  6680  fnrel  6681  funfni  6685  fncofn  6696  fnco  6697  fncoOLD  6698  fnssresb  6702  ffun  6750  f1fun  6819  f1ofun  6864  fnbrfvb  6973  fvelimad  6989  fvelimab  6994  fvun1  7013  elpreima  7091  respreima  7099  rescnvimafod  7107  fnsnr  7199  fnprb  7245  fntpb  7246  fconst3  7250  fnfvima  7270  ralima  7274  fnunirn  7291  nvof1o  7316  f1eqcocnv  7337  offun  7728  fnexALT  7991  curry1  8145  curry2  8148  fimaproj  8176  suppvalfng  8208  suppvalfn  8209  suppfnss  8230  fnsuppres  8232  frrlem2  8328  frrlem12  8338  wfrlem2OLD  8365  wfrlem14OLD  8378  tfrlem4  8435  tfrlem5  8436  tfrlem11  8444  tz7.48-2  8498  tz7.49  8501  naddcllem  8732  naddov2  8735  naddunif  8749  naddasslem1  8750  naddasslem2  8751  fndmeng  9100  fnfi  9244  fodomfi  9378  fodomfiOLD  9398  resfnfinfin  9405  fczfsuppd  9455  marypha2lem4  9507  inf0  9690  r1elss  9875  dfac8alem  10098  alephfp  10177  dfac3  10190  dfac9  10206  dfac12lem1  10213  dfac12lem2  10214  r1om  10312  cfsmolem  10339  alephsing  10345  zorn2lem1  10565  zorn2lem5  10569  zorn2lem6  10570  zorn2lem7  10571  ttukeylem3  10580  ttukeylem6  10583  fnct  10606  smobeth  10655  fpwwe2lem8  10707  wunr1om  10788  tskr1om  10836  tskr1om2  10837  uzrdg0i  14010  uzrdgsuci  14011  seqexw  14068  hashkf  14381  cshimadifsn  14878  cshimadifsn0  14879  shftfn  15122  phimullem  16826  imasaddvallem  17589  imasvscaval  17598  dfrngc2  20650  dfringc2  20679  rngcresringcat  20691  lidlval  21243  rspval  21244  psgnghm  21621  iscldtop  23124  2ndcomap  23487  qtoptop  23729  basqtop  23740  qtoprest  23746  kqfvima  23759  isr0  23766  kqreglem1  23770  kqnrmlem1  23772  kqnrmlem2  23773  ustbas  24257  uniiccdif  25632  noextendseq  27730  madeval  27909  oldval  27911  addsval  28013  negsval  28075  negsproplem2  28079  negsunif  28105  mulsval  28153  zsex  28384  fcoinver  32626  fnpreimac  32689  mdetpmtr1  33769  sseqf  34357  sseqfv2  34359  elorrvc  34428  bnj1371  35005  bnj1497  35036  fnrelpredd  35065  gblacfnacd  35075  filnetlem4  36347  heibor1lem  37769  diaf11N  41006  dibf11N  41118  dibclN  41119  dihintcl  41301  aks6d1c2lem4  42084  fnsnbt  42225  ismrc  42657  dnnumch1  43001  aomclem4  43014  aomclem6  43016  tfsconcatrev  43310  tfsnfin  43314  fnimafnex  43402  ntrclsfv1  44017  ntrneifv1  44041  finnzfsuppd  44171  fvelima2  45169  climrescn  45669  icccncfext  45808  stoweidlem29  45950  stoweidlem59  45980  ovolval4lem1  46570  fnresfnco  46956  funcoressn  46957  fnfocofob  46994  fnbrafvb  47069  tz6.12-afv  47088  afvco2  47091  tz6.12-afv2  47155  fnbrafv2b  47163  imaelsetpreimafv  47269  imasetpreimafvbijlemfv  47276  imasetpreimafvbijlemfo  47279  plusfreseq  47887  ackvalsuc0val  48421