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

Theorem fnfun 6598
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 6495 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simplbi 499 1 (𝐹 Fn 𝐴 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  dom cdm 5631  Fun wfun 6486   Fn wfn 6487
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 398  df-fn 6495
This theorem is referenced by:  fnfund  6599  fnrel  6600  funfni  6604  fncofn  6613  fnco  6614  fncoOLD  6615  fnssresb  6619  ffun  6667  f1fun  6736  f1ofun  6782  fnbrfvb  6891  fvelimad  6905  fvelimab  6910  fvun1  6928  elpreima  7004  respreima  7012  rescnvimafod  7020  fnsnr  7106  fnprb  7153  fntpb  7154  fconst3  7158  fnfvima  7178  fnunirn  7196  nvof1o  7221  f1eqcocnv  7242  f1eqcocnvOLD  7243  offun  7622  fnexALT  7874  curry1  8025  curry2  8028  fimaproj  8056  suppvalfng  8067  suppvalfn  8068  suppfnss  8088  fnsuppres  8090  frrlem2  8186  frrlem12  8196  wfrlem2OLD  8223  wfrlem14OLD  8236  tfrlem4  8293  tfrlem5  8294  tfrlem11  8302  tz7.48-2  8356  tz7.49  8359  fndmeng  8913  fnfi  9059  fodomfi  9203  resfnfinfin  9210  fczfsuppd  9257  marypha2lem4  9308  inf0  9491  r1elss  9676  dfac8alem  9899  alephfp  9978  dfac3  9991  dfac9  10006  dfac12lem1  10013  dfac12lem2  10014  r1om  10114  cfsmolem  10140  alephsing  10146  zorn2lem1  10366  zorn2lem5  10370  zorn2lem6  10371  zorn2lem7  10372  ttukeylem3  10381  ttukeylem6  10384  fnct  10407  smobeth  10456  fpwwe2lem8  10508  wunr1om  10589  tskr1om  10637  tskr1om2  10638  uzrdg0i  13793  uzrdgsuci  13794  seqexw  13851  hashkf  14160  cshimadifsn  14650  cshimadifsn0  14651  shftfn  14892  phimullem  16586  imasaddvallem  17346  imasvscaval  17355  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  31310  fnpreimac  31372  mdetpmtr1  32165  sseqf  32753  sseqfv2  32755  elorrvc  32824  bnj1371  33402  bnj1497  33433  fnrelpredd  33454  naddcllem  34208  naddov2  34211  naddunif  34223  naddasslem1  34224  naddasslem2  34225  addsval  34259  negsval  34299  filnetlem4  34739  heibor1lem  36154  diaf11N  39398  dibf11N  39510  dibclN  39511  dihintcl  39693  fnsnbt  40541  ismrc  40858  dnnumch1  41205  aomclem4  41218  aomclem6  41220  fnimafnex  41443  ntrclsfv1  42060  ntrneifv1  42084  finnzfsuppd  42215  fvelima2  43208  climrescn  43699  icccncfext  43838  stoweidlem29  43980  stoweidlem59  44010  ovolval4lem1  44598  fnresfnco  44975  funcoressn  44976  fnfocofob  45011  fnbrafvb  45086  tz6.12-afv  45105  afvco2  45108  tz6.12-afv2  45172  fnbrafv2b  45180  imaelsetpreimafv  45287  imasetpreimafvbijlemfv  45294  imasetpreimafvbijlemfo  45297  plusfreseq  45766  dfrngc2  45970  dfringc2  46016  rngcresringcat  46028  ackvalsuc0val  46473
  Copyright terms: Public domain W3C validator