Theorem fnfun 6636

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5659  Fun wfun 6531   Fn wfn 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6540

This theorem is used by:  fnfund  6637  fnrel  6638  funfni  6642  fncofn  6653  fnco  6654  fnssresb  6658  ffunOLD  6710  f1funOLD  6778  f1ofun  6823  fnbrfvb  6932  fvelima2  6934  fvelimad  6949  fvelimab  6954  fvun1  6973  elpreima  7054  respreima  7062  rescnvimafod  7070  fnsnr  7165  fnsnbg  7166  fnprb  7211  fntpb  7212  fconst3  7216  fnfvima  7236  ralima  7240  fnunirn  7254  nvof1o  7285  f1eqcocnv  7306  offun  7696  fnexALT  7952  curry1  8105  curry2  8108  fimaproj  8137  suppvalfng  8169  suppvalfn  8170  suppfnss  8191  fnsuppres  8193  frrlem2  8290  frrlem12  8300  tfrlem4  8371  tfrlem5  8372  tfrlem11  8381  tz7.48-2  8435  tz7.49  8438  naddcllem  8668  naddov2  8671  naddunif  8686  naddasslem1  8687  naddasslem2  8688  fndmeng  9046  fnfi  9176  fodomfi  9286  resfnfinfin  9308  tfsnfin2  9334  finnzfsuppd  9347  fczfsuppd  9360  marypha2lem4  9412  inf0  9604  r1elss  9792  dfac8alem  10036  alephfp  10115  dfac3  10128  dfac9  10143  dfac12lem1  10150  dfac12lem2  10151  r1om  10249  cfsmolem  10276  alephsing  10282  zorn2lem1  10502  zorn2lem5  10506  zorn2lem6  10507  zorn2lem7  10508  ttukeylem3  10517  ttukeylem6  10520  fnct  10548  fnctOLD  10549  smobeth  10599  fpwwe2lem8  10651  wunr1om  10732  tskr1om  10780  tskr1om2  10781  uzrdg0i  14027  uzrdgsuci  14028  seqexw  14085  hashkf  14400  cshimadifsn  14904  cshimadifsn0  14905  shftfn  15150  phimullem  16876  imasaddvallem  17621  imasvscaval  17630  dfrngc2  20796  dfringc2  20825  rngcresringcat  20837  lidlval  21403  rspval  21404  psgnghm  21799  iscldtop  23326  2ndcomap  23690  qtoptop  23932  basqtop  23943  qtoprest  23949  kqfvima  23962  isr0  23969  kqreglem1  23973  kqnrmlem1  23975  kqnrmlem2  23976  ustbas  24459  uniiccdif  25812  noextendseq  27911  madeval  28105  oldval  28107  addsval  28235  negsval  28298  negsproplem2  28302  negsunif  28328  mulsval  28382  zsex  28653  nowisdomv  30962  fcoinver  33085  fresunsn  33106  fnpreimac  33151  elrgspnlem2  33691  mdetpmtr1  34341  sseqf  34911  sseqfv2  34913  elorrvc  34983  bnj1371  35546  bnj1497  35577  fnrelpredd  35604  gblacfnacd  35707  onvf1odlem3  35710  onvf1odlem4  35711  onvf1od  35712  nmulprop  36778  filnetlem4  37008  heibor1lem  38567  diaf11N  41930  dibf11N  42042  dibclN  42043  dihintcl  42225  aks6d1c2lem4  43001  ismrc  43554  dnnumch1  43893  aomclem4  43906  aomclem6  43908  tfsconcatrev  44197  tfsnfin  44201  fnimafnex  44288  ntrclsfv1  44903  ntrneifv1  44927  climrescn  46584  icccncfext  46723  stoweidlem29  46865  stoweidlem59  46895  ovolval4lem1  47485  fnresfnco  47937  funcoressn  47938  fnfocofob  47975  fnbrafvb  48050  tz6.12-afv  48069  afvco2  48072  tz6.12-afv2  48136  fnbrafv2b  48144  imaelsetpreimafv  48303  imasetpreimafvbijlemfv  48310  imasetpreimafvbijlemfo  48313  plusfreseq  49087  ackvalsuc0val  49625