Theorem fnfun 6149

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

Syntax hints:   → wi 4   = wceq 1632  dom cdm 5266  Fun wfun 6043   Fn wfn 6044

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 385  df-fn 6052

This theorem is referenced by:  fnrel  6150  funfni  6152  fnco  6160  fnssresb  6164  ffun  6209  f1fun  6264  f1ofun  6300  fnbrfvb  6397  fvelimab  6415  fvun1  6431  elpreima  6500  respreima  6507  fnsnr  6595  fnprb  6636  fntpb  6637  fconst3  6641  fnfvima  6659  fnunirn  6674  nvof1o  6699  f1eqcocnv  6719  fnexALT  7297  curry1  7437  curry2  7440  suppvalfn  7470  suppfnss  7488  suppfnssOLD  7489  fnsuppres  7491  wfrlem2  7584  wfrlem14  7597  tfrlem4  7644  tfrlem5  7645  tfrlem11  7653  tz7.48-2  7706  tz7.49  7709  fndmeng  8199  fnfi  8403  fodomfi  8404  resfnfinfin  8411  fczfsuppd  8458  marypha2lem4  8509  inf0  8691  r1elss  8842  dfac8alem  9042  alephfp  9121  dfac3  9134  dfac9  9150  dfac12lem1  9157  dfac12lem2  9158  r1om  9258  cfsmolem  9284  alephsing  9290  zorn2lem1  9510  zorn2lem5  9514  zorn2lem6  9515  zorn2lem7  9516  ttukeylem3  9525  ttukeylem6  9528  fnct  9551  smobeth  9600  fpwwe2lem9  9652  wunr1om  9733  tskr1om  9781  tskr1om2  9782  uzrdg0i  12952  uzrdgsuci  12953  hashkf  13313  cshimadifsn  13775  cshimadifsn0  13776  shftfn  14012  phimullem  15686  imasaddvallem  16391  imasvscaval  16400  frmdss2  17601  lcomfsupp  19105  lidlval  19394  rspval  19395  psrbagev1  19712  psgnghm  20128  frlmsslsp  20337  iscldtop  21101  2ndcomap  21463  qtoptop  21705  basqtop  21716  qtoprest  21722  kqfvima  21735  isr0  21742  kqreglem1  21746  kqnrmlem1  21748  kqnrmlem2  21749  elrnust  22229  ustbas  22232  uniiccdif  23546  fcoinver  29725  mdetpmtr1  30198  fimaproj  30209  sseqf  30763  sseqfv2  30765  elorrvc  30834  bnj930  31147  bnj1371  31404  bnj1497  31435  frrlem2  32087  noextendseq  32126  madeval  32241  filnetlem4  32682  heibor1lem  33921  diaf11N  36840  dibf11N  36952  dibclN  36953  dihintcl  37135  ismrc  37766  dnnumch1  38116  aomclem4  38129  aomclem6  38131  ntrclsfv1  38855  ntrneifv1  38879  fvelimad  39957  fnfvimad  39958  fvelima2  39974  climrescn  40483  icccncfext  40603  stoweidlem29  40749  stoweidlem59  40779  ovolval4lem1  41369  fnresfnco  41712  funcoressn  41713  fnbrafvb  41740  tz6.12-afv  41759  afvco2  41762  plusfreseq  42282  dfrngc2  42482  dfringc2  42528  rngcresringcat  42540  mndpsuppss  42662  mndpfsupp  42667