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

Theorem fnfun 6597
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 6494 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simplbi 498 1 (𝐹 Fn 𝐴 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  dom cdm 5630  Fun wfun 6485   Fn wfn 6486
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 206  df-an 397  df-fn 6494
This theorem is referenced by:  fnfund  6598  fnrel  6599  funfni  6603  fncofn  6612  fnco  6613  fncoOLD  6614  fnssresb  6618  ffun  6666  f1fun  6735  f1ofun  6781  fnbrfvb  6890  fvelimad  6904  fvelimab  6909  fvun1  6927  elpreima  7003  respreima  7011  rescnvimafod  7019  fnsnr  7105  fnprb  7152  fntpb  7153  fconst3  7157  fnfvima  7177  fnunirn  7195  nvof1o  7220  f1eqcocnv  7241  f1eqcocnvOLD  7242  offun  7621  fnexALT  7873  curry1  8024  curry2  8027  fimaproj  8055  suppvalfng  8066  suppvalfn  8067  suppfnss  8087  fnsuppres  8089  frrlem2  8185  frrlem12  8195  wfrlem2OLD  8222  wfrlem14OLD  8235  tfrlem4  8292  tfrlem5  8293  tfrlem11  8301  tz7.48-2  8355  tz7.49  8358  fndmeng  8912  fnfi  9058  fodomfi  9202  resfnfinfin  9209  fczfsuppd  9256  marypha2lem4  9307  inf0  9490  r1elss  9675  dfac8alem  9898  alephfp  9977  dfac3  9990  dfac9  10005  dfac12lem1  10012  dfac12lem2  10013  r1om  10113  cfsmolem  10139  alephsing  10145  zorn2lem1  10365  zorn2lem5  10369  zorn2lem6  10370  zorn2lem7  10371  ttukeylem3  10380  ttukeylem6  10383  fnct  10406  smobeth  10455  fpwwe2lem8  10507  wunr1om  10588  tskr1om  10636  tskr1om2  10637  uzrdg0i  13792  uzrdgsuci  13793  seqexw  13850  hashkf  14159  cshimadifsn  14649  cshimadifsn0  14650  shftfn  14891  phimullem  16585  imasaddvallem  17345  imasvscaval  17354  lidlval  20584  rspval  20585  psgnghm  20907  iscldtop  22368  2ndcomap  22731  qtoptop  22973  basqtop  22984  qtoprest  22990  kqfvima  23003  isr0  23010  kqreglem1  23014  kqnrmlem1  23016  kqnrmlem2  23017  ustbas  23501  uniiccdif  24864  noextendseq  26937  madeval  27103  oldval  27105  fcoinver  31322  fnpreimac  31384  mdetpmtr1  32177  sseqf  32765  sseqfv2  32767  elorrvc  32836  bnj1371  33414  bnj1497  33445  fnrelpredd  33466  naddcllem  34220  naddov2  34223  naddunif  34235  naddasslem1  34236  naddasslem2  34237  addsval  34265  negsval  34306  negsproplem2  34309  filnetlem4  34748  heibor1lem  36163  diaf11N  39407  dibf11N  39519  dibclN  39520  dihintcl  39702  fnsnbt  40550  ismrc  40889  dnnumch1  41236  aomclem4  41249  aomclem6  41251  fnimafnex  41474  ntrclsfv1  42091  ntrneifv1  42115  finnzfsuppd  42246  fvelima2  43245  climrescn  43742  icccncfext  43881  stoweidlem29  44023  stoweidlem59  44053  ovolval4lem1  44643  fnresfnco  45024  funcoressn  45025  fnfocofob  45060  fnbrafvb  45135  tz6.12-afv  45154  afvco2  45157  tz6.12-afv2  45221  fnbrafv2b  45229  imaelsetpreimafv  45336  imasetpreimafvbijlemfv  45343  imasetpreimafvbijlemfo  45346  plusfreseq  45815  dfrngc2  46019  dfringc2  46065  rngcresringcat  46077  ackvalsuc0val  46522
  Copyright terms: Public domain W3C validator