Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnfun Structured version   Visualization version   GIF version

Theorem fnfun 6431
 Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fnfun (𝐹 Fn 𝐴 → Fun 𝐹)

Proof of Theorem fnfun
StepHypRef Expression
1 df-fn 6335 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simplbi 501 1 (𝐹 Fn 𝐴 → Fun 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538  dom cdm 5523  Fun wfun 6326   Fn wfn 6327 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 210  df-an 400  df-fn 6335 This theorem is referenced by:  fnrel  6432  funfni  6436  fnco  6445  fnssresb  6449  ffun  6498  f1fun  6559  f1ofun  6601  fnbrfvb  6703  fvelimad  6717  fvelimab  6722  fvun1  6739  elpreima  6815  respreima  6823  fnsnr  6914  fnprb  6958  fntpb  6959  fconst3  6963  fnfvima  6983  fnunirn  7000  nvof1o  7025  f1eqcocnv  7045  f1eqcocnvOLD  7046  offun  7413  fnexALT  7647  curry1  7795  curry2  7798  fimaproj  7825  suppvalfng  7833  suppvalfn  7834  suppfnss  7854  fnsuppres  7856  wfrlem2  7956  wfrlem14  7969  tfrlem4  8016  tfrlem5  8017  tfrlem11  8025  tz7.48-2  8079  tz7.49  8082  fndmeng  8588  fnfi  8798  fodomfi  8799  resfnfinfin  8806  fczfsuppd  8853  marypha2lem4  8904  inf0  9086  r1elss  9237  dfac8alem  9458  alephfp  9537  dfac3  9550  dfac9  9565  dfac12lem1  9572  dfac12lem2  9573  r1om  9673  cfsmolem  9699  alephsing  9705  zorn2lem1  9925  zorn2lem5  9929  zorn2lem6  9930  zorn2lem7  9931  ttukeylem3  9940  ttukeylem6  9943  fnct  9966  smobeth  10015  fpwwe2lem8  10067  wunr1om  10148  tskr1om  10196  tskr1om2  10197  uzrdg0i  13342  uzrdgsuci  13343  seqexw  13400  hashkf  13708  cshimadifsn  14202  cshimadifsn0  14203  shftfn  14444  phimullem  16126  imasaddvallem  16814  imasvscaval  16823  lidlval  19978  rspval  19979  psgnghm  20291  iscldtop  21741  2ndcomap  22104  qtoptop  22346  basqtop  22357  qtoprest  22363  kqfvima  22376  isr0  22383  kqreglem1  22387  kqnrmlem1  22389  kqnrmlem2  22390  elrnust  22871  ustbas  22874  uniiccdif  24223  fcoinver  30414  fnpreimac  30478  mdetpmtr1  31242  sseqf  31826  sseqfv2  31828  elorrvc  31897  bnj930  32217  bnj1371  32477  bnj1497  32508  fnrelpredd  32538  frrlem2  33307  frrlem12  33317  noextendseq  33357  madeval  33517  oldval  33519  filnetlem4  33989  heibor1lem  35398  diaf11N  38496  dibf11N  38608  dibclN  38609  dihintcl  38791  fnsnbt  39566  ismrc  39813  dnnumch1  40159  aomclem4  40172  aomclem6  40174  ntrclsfv1  40929  ntrneifv1  40953  finnzfsuppd  41086  fvelima2  42066  climrescn  42558  icccncfext  42697  stoweidlem29  42839  stoweidlem59  42869  ovolval4lem1  43456  fnresfnco  43801  funcoressn  43802  fnbrafvb  43878  tz6.12-afv  43897  afvco2  43900  tz6.12-afv2  43964  fnbrafv2b  43972  imaelsetpreimafv  44080  imasetpreimafvbijlemfv  44087  imasetpreimafvbijlemfo  44090  plusfreseq  44560  dfrngc2  44764  dfringc2  44810  rngcresringcat  44822  ackvalsuc0val  45267
 Copyright terms: Public domain W3C validator