Theorem fnfun 6617

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

Syntax hints:   → wi 4   = wceq 1559  dom cdm 5645  Fun wfun 6511   Fn wfn 6512

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 209  df-an 400  df-fn 6520

This theorem is referenced by:  fnfund  6618  fnrel  6619  funfni  6623  fncofn  6634  fnco  6635  fnssresb  6639  ffunOLD  6691  f1funOLD  6759  f1ofun  6804  fnbrfvb  6913  fvelima2  6915  fvelimad  6930  fvelimab  6935  fvun1  6954  elpreima  7035  respreima  7043  rescnvimafod  7050  fnsnr  7143  fnsnbg  7144  fnprb  7188  fntpb  7189  fconst3  7193  fnfvima  7213  ralima  7217  fnunirn  7233  nvof1o  7260  f1eqcocnv  7281  offun  7670  fnexALT  7928  curry1  8078  curry2  8081  fimaproj  8110  suppvalfng  8142  suppvalfn  8143  suppfnss  8164  fnsuppres  8166  frrlem2  8263  frrlem12  8273  tfrlem4  8344  tfrlem5  8345  tfrlem11  8354  tz7.48-2  8408  tz7.49  8411  naddcllem  8641  naddov2  8644  naddunif  8659  naddasslem1  8660  naddasslem2  8661  fndmeng  9012  fnfi  9142  fodomfi  9252  fodomfiOLD  9270  resfnfinfin  9277  tfsnfin2  9303  finnzfsuppd  9316  fczfsuppd  9329  marypha2lem4  9381  inf0  9573  r1elss  9761  dfac8alem  9982  alephfp  10061  dfac3  10074  dfac9  10090  dfac12lem1  10097  dfac12lem2  10098  r1om  10196  cfsmolem  10224  alephsing  10230  zorn2lem1  10450  zorn2lem5  10454  zorn2lem6  10455  zorn2lem7  10456  ttukeylem3  10465  ttukeylem6  10468  fnct  10491  smobeth  10541  fpwwe2lem8  10593  wunr1om  10674  tskr1om  10722  tskr1om2  10723  uzrdg0i  13969  uzrdgsuci  13970  seqexw  14027  hashkf  14342  cshimadifsn  14839  cshimadifsn0  14840  shftfn  15083  phimullem  16797  imasaddvallem  17542  imasvscaval  17551  dfrngc2  20657  dfringc2  20686  rngcresringcat  20698  lidlval  21260  rspval  21261  psgnghm  21612  iscldtop  23135  2ndcomap  23498  qtoptop  23740  basqtop  23751  qtoprest  23757  kqfvima  23770  isr0  23777  kqreglem1  23781  kqnrmlem1  23783  kqnrmlem2  23784  ustbas  24267  uniiccdif  25620  noextendseq  27708  madeval  27902  oldval  27904  addsval  28032  negsval  28095  negsproplem2  28099  negsunif  28125  mulsval  28179  zsex  28450  nowisdomv  30622  fcoinver  32753  fresunsn  32777  fnpreimac  32822  elrgspnlem2  33385  mdetpmtr1  34081  sseqf  34650  sseqfv2  34652  elorrvc  34722  bnj1371  35288  bnj1497  35319  fnrelpredd  35351  gblacfnacd  35409  onvf1odlem3  35412  onvf1odlem4  35413  onvf1od  35414  nmulprop  36504  filnetlem4  36705  heibor1lem  38272  diaf11N  41637  dibf11N  41749  dibclN  41750  dihintcl  41932  aks6d1c2lem4  42708  ismrc  43246  dnnumch1  43585  aomclem4  43598  aomclem6  43600  tfsconcatrev  43889  tfsnfin  43893  fnimafnex  43980  ntrclsfv1  44595  ntrneifv1  44619  climrescn  46286  icccncfext  46425  stoweidlem29  46567  stoweidlem59  46597  ovolval4lem1  47187  fnresfnco  47599  funcoressn  47600  fnfocofob  47637  fnbrafvb  47712  tz6.12-afv  47731  afvco2  47734  tz6.12-afv2  47798  fnbrafv2b  47806  imaelsetpreimafv  47965  imasetpreimafvbijlemfv  47972  imasetpreimafvbijlemfo  47975  plusfreseq  48750  ackvalsuc0val  49273