MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elmapi Unicode version

Theorem elmapi 7460
Description: A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)
Assertion
Ref Expression
elmapi

Proof of Theorem elmapi
StepHypRef Expression
1 elmapex 7459 . . 3
2 elmapg 7452 . . 3
31, 2syl 16 . 2
43ibi 241 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  e.wcel 1818   cvv 3109  -->wf 5589  (class class class)co 6296   cmap 7439
This theorem is referenced by:  elmapfn  7461  elmapfun  7462  elmapssres  7463  mapsspm  7472  map0b  7477  mapss  7481  mapsncnv  7485  ralxpmap  7488  mapen  7701  mapxpen  7703  mapunen  7706  mapfienlem1  7884  mapfienlem2  7885  mapfienlem3  7886  mapfien  7887  wemaplem2  7993  wemappo  7995  wemapsolem  7996  wemapso  7997  wemapso2OLD  7998  wemapso2lem  7999  cantnffvalOLD  8103  mapfienOLD  8159  wemapwe  8160  wemapweOLD  8161  iunmapdisj  8425  fseqenlem1  8426  fseqenlem2  8427  numacn  8451  finacn  8452  acndom  8453  acndom2  8456  infpwfien  8464  infmap2  8619  fin23lem40  8752  isf32lem12  8765  isf34lem6  8781  acncc  8841  pwfseqlem3  9059  pwxpndom2  9064  ramval  14526  ramub  14531  ramcl  14547  imasdsval2  14913  funcf2  15237  funcpropd  15269  fsfnn0gsumfsffz  17011  gsummptnn0fzfv  17016  mplbas2  18134  ltbwe  18137  psr1baslem  18224  psr1basf  18240  fvcoe1  18246  coe1mul2lem1  18308  ply1coe  18337  ply1coeOLD  18338  frlmfibas  18795  frlmbas3  18807  frlmipval  18810  frlmphllem  18811  frlmphl  18812  elfilspd  18838  islindf4  18873  mamures  18892  mndvcl  18893  mndvass  18894  mndvlid  18895  mndvrid  18896  grpvlinv  18897  grpvrinv  18898  mhmvlin  18899  mamucl  18903  mamuass  18904  mamudi  18905  mamudir  18906  mamuvs1  18907  mamuvs2  18908  mamulid  18943  mamurid  18944  mattposcl  18955  mattpostpos  18956  tposmap  18959  mamutpos  18960  matgsumcl  18962  mavmulcl  19049  mavmulass  19051  mavmulsolcl  19053  marepvcl  19071  1marepvmarrepid  19077  mdetleib2  19090  mdetf  19097  mdetdiaglem  19100  mdetrlin  19104  mdetrsca  19105  mdetralt  19110  mdetunilem7  19120  mdetunilem9  19122  maducoeval2  19142  madutpos  19144  madugsum  19145  madurid  19146  cramerimplem1  19185  m2pmfzmap  19248  decpmatval  19266  pmatcollpw3lem  19284  pmatcollpw3fi1lem1  19287  pmatcollpw3fi1lem2  19288  pm2mp  19326  chfacfisf  19355  chfacfisfcpmat  19356  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  chfacfpmmulgsum2  19366  cayhamlem1  19367  cpmadugsumlemF  19377  cpmadugsumfi  19378  cayhamlem2  19385  chcoeffeqlem  19386  cayleyhamilton1  19393  pnrmopn  19844  xkoptsub  20155  xkopt  20156  tmdgsum  20594  imasdsf1olem  20876  rrxnm  21823  rrxds  21825  rrxf  21828  rrxmvallem  21831  ehlbase  21838  ovolscalem2  21925  uniioombl  21998  tdeglem2  22459  plypf1  22609  ulmclm  22782  ulmcaulem  22789  ulmcau  22790  ulmss  22792  ulmbdd  22793  ulmcn  22794  ulmdvlem1  22795  ulmdvlem2  22796  ulmdvlem3  22797  mtest  22799  mtestbdd  22800  mbfulm  22801  iblulm  22802  itgulm  22803  itgulm2  22804  adjval2  26810  fcobijfs  27549  resf1o  27553  fpwrelmap  27556  mbfmf  28226  elmbfmvol2  28238  eulerpartlemelr  28296  eulerpartlemf  28309  eulerpartlemt  28310  eulerpartgbij  28311  eulerpartlemgu  28316  eulerpartlemgh  28317  eulerpartlemgf  28318  eulerpartlemgs2  28319  mrsubff1  28874  mrsub0  28876  mrsubf  28877  mrsubccat  28878  mrsubcn  28879  msubrn  28889  msubff  28890  msubf  28892  msubff1  28916  mclsind  28930  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  rrnmet  30325  rrndstprj1  30326  rrndstprj2  30327  rrncmslem  30328  rrnequiv  30331  mapco2g  30646  mapfzcons1  30649  mapfzcons2  30651  mzpcompact2lem  30684  eldiophb  30690  elmapresaun  30704  elmapresaunres2  30705  eq0rabdioph  30710  rexrabdioph  30727  eldioph4b  30745  diophren  30747  rmydioph  30956  rmxdioph  30958  expdiophlem2  30964  expdioph  30965  pw2f1o2val2  30982  wepwsolem  30987  pwfi2f1o  31044  mccllem  31605  dvnprodlem1  31743  dvnprodlem2  31744  fourierdlem11  31900  fourierdlem12  31901  fourierdlem13  31902  fourierdlem14  31903  fourierdlem34  31923  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem54  31943  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem69  31958  fourierdlem72  31961  fourierdlem74  31963  fourierdlem75  31964  fourierdlem79  31968  fourierdlem85  31974  fourierdlem88  31977  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem94  31983  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem113  32002  etransclem24  32041  etransclem26  32043  etransclem27  32044  etransclem28  32045  etransclem31  32048  etransclem32  32049  etransclem33  32050  etransclem34  32051  etransclem35  32052  etransclem37  32054  etransclem38  32055  intop  32527  assintop  32533  isassintop  32534  funcestrcsetclem8  32653  funcestrcsetclem9  32654  funcsetcestrclem8  32668  funcsetcestrclem9  32669  ofaddmndmap  32933  rmsupp0  32961  domnmsuppn0  32962  rmsuppss  32963  mndpsuppss  32964  scmsuppss  32965  gsumlsscl  32976  lincfsuppcl  33014  linccl  33015  lcosn0  33021  lincdifsn  33025  lincsum  33030  lincscm  33031  lincscmcl  33033  islinindfis  33050  lincext1  33055  lincext2  33056  lincext3  33057  lindslinindimp2lem1  33059  lindslinindimp2lem2  33060  lindslinindimp2lem4  33062  lindslinindsimp2lem5  33063  snlindsntor  33072  lincresunitlem2  33077  lincresunit3lem1  33080  lincresunit3lem2  33081  lincresunit3  33082  lincreslvec3  33083  isldepslvec2  33086  zlmodzxzldeplem2  33102  zlmodzxzldeplem3  33103  ldepsnlinclem1  33106  ldepsnlinclem2  33107  aacllem  33216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-1st 6800  df-2nd 6801  df-map 7441
  Copyright terms: Public domain W3C validator