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

Theorem elmapi 7921
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 7920 . . 3 (𝐴 ∈ (𝐵𝑚 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2 elmapg 7912 . . 3 ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵𝑚 𝐶) ↔ 𝐴:𝐶𝐵))
31, 2syl 17 . 2 (𝐴 ∈ (𝐵𝑚 𝐶) → (𝐴 ∈ (𝐵𝑚 𝐶) ↔ 𝐴:𝐶𝐵))
43ibi 256 1 (𝐴 ∈ (𝐵𝑚 𝐶) → 𝐴:𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wcel 2030  Vcvv 3231  wf 5922  (class class class)co 6690  𝑚 cmap 7899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-map 7901
This theorem is referenced by:  elmapfn  7922  elmapfun  7923  elmapssres  7924  mapsspm  7933  map0b  7938  mapss  7942  mapsncnv  7946  ralxpmap  7949  mapen  8165  mapxpen  8167  mapunen  8170  mapfienlem1  8351  mapfienlem2  8352  mapfienlem3  8353  mapfien  8354  wemaplem2  8493  wemappo  8495  wemapsolem  8496  wemapso  8497  wemapso2lem  8498  wemapwe  8632  iunmapdisj  8884  fseqenlem1  8885  fseqenlem2  8886  numacn  8910  finacn  8911  acndom  8912  acndom2  8915  infpwfien  8923  infmap2  9078  fin23lem40  9211  isf32lem12  9224  isf34lem6  9240  acncc  9300  pwfseqlem3  9520  pwxpndom2  9525  ramval  15759  ramub  15764  ramcl  15780  prmgaplem7  15808  prmgaplem8  15809  imasdsval2  16223  funcf2  16575  funcpropd  16607  funcestrcsetclem8  16834  funcestrcsetclem9  16835  funcsetcestrclem8  16849  funcsetcestrclem9  16850  fsfnn0gsumfsffz  18425  gsummptnn0fzfv  18430  mplbas2  19518  ltbwe  19520  psr1baslem  19603  psr1basf  19619  fvcoe1  19625  coe1mul2lem1  19685  ply1coe  19714  frlmfibas  20153  frlmbas3  20163  frlmipval  20166  frlmphllem  20167  frlmphl  20168  elfilspd  20190  islindf4  20225  mamures  20244  mndvcl  20245  mndvass  20246  mndvlid  20247  mndvrid  20248  grpvlinv  20249  grpvrinv  20250  mhmvlin  20251  mamucl  20255  mamuass  20256  mamudi  20257  mamudir  20258  mamuvs1  20259  mamuvs2  20260  mamulid  20295  mamurid  20296  mattposcl  20307  mattpostpos  20308  tposmap  20311  mamutpos  20312  matgsumcl  20314  mavmulcl  20401  mavmulass  20403  mavmulsolcl  20405  marepvcl  20423  1marepvmarrepid  20429  mdetleib2  20442  mdetf  20449  mdetdiaglem  20452  mdetrlin  20456  mdetrsca  20457  mdetralt  20462  mdetunilem7  20472  mdetunilem9  20474  maducoeval2  20494  madutpos  20496  madugsum  20497  madurid  20498  cramerimplem1  20537  m2pmfzmap  20600  decpmatval  20618  pmatcollpw3lem  20636  pmatcollpw3fi1lem1  20639  pmatcollpw3fi1lem2  20640  pm2mp  20678  chfacfisf  20707  chfacfisfcpmat  20708  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  chfacfpmmulgsum2  20718  cayhamlem1  20719  cpmadugsumlemF  20729  cpmadugsumfi  20730  cayhamlem2  20737  chcoeffeqlem  20738  cayleyhamilton1  20745  pnrmopn  21195  xkoptsub  21505  xkopt  21506  tmdgsum  21946  imasdsf1olem  22225  rrxnm  23225  rrxds  23227  rrxf  23230  rrxmvallem  23233  ehlbase  23240  ovolscalem2  23328  uniioombl  23403  tdeglem2  23866  plypf1  24013  ulmclm  24186  ulmcaulem  24193  ulmcau  24194  ulmss  24196  ulmbdd  24197  ulmcn  24198  ulmdvlem1  24199  ulmdvlem2  24200  ulmdvlem3  24201  mtest  24203  mtestbdd  24204  mbfulm  24205  iblulm  24206  itgulm  24207  itgulm2  24208  adjval2  28878  fmptco1f1o  29562  fcobijfs  29629  resf1o  29633  fpwrelmap  29636  smatrcl  29990  mbfmf  30445  elmbfmvol2  30457  eulerpartlemelr  30547  eulerpartlemf  30560  eulerpartlemt  30561  eulerpartgbij  30562  eulerpartlemgu  30567  eulerpartlemgh  30568  eulerpartlemgf  30569  eulerpartlemgs2  30570  reprf  30818  reprsuc  30821  vtsprod  30845  circlemethhgt  30849  tgoldbachgtd  30868  mrsubff1  31537  mrsub0  31539  mrsubf  31540  mrsubccat  31541  mrsubcn  31542  msubrn  31552  msubff  31553  msubf  31555  msubff1  31579  mclsind  31593  uncf  33518  curunc  33521  unccur  33522  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  poimir  33572  broucube  33573  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  rrnmet  33758  rrndstprj1  33759  rrndstprj2  33760  rrncmslem  33761  rrnequiv  33764  mapco2g  37594  mapfzcons1  37597  mapfzcons2  37599  mzpcompact2lem  37631  eldiophb  37637  elmapresaun  37651  elmapresaunres2  37652  eq0rabdioph  37657  rexrabdioph  37675  eldioph4b  37692  diophren  37694  rmydioph  37898  rmxdioph  37900  expdiophlem2  37906  expdioph  37907  pw2f1o2val2  37924  wepwsolem  37929  pwfi2f1o  37983  rfovcnvf1od  38615  rfovcnvfvd  38618  fsovrfovd  38620  fsovcnvlem  38624  ntrk0kbimka  38654  neik0pk1imk0  38662  ntrclsfveq1  38675  ntrclsfveq2  38676  ntrclsfveq  38677  ntrclsss  38678  ntrclsiso  38682  ntrclsk2  38683  ntrclskb  38684  ntrclsk3  38685  ntrclsk13  38686  ntrclsk4  38687  ntrneifv3  38697  ntrneineine0lem  38698  ntrneineine1lem  38699  ntrneifv4  38700  ntrneiel2  38701  ntrneicls00  38704  ntrneicls11  38705  ntrneiiso  38706  ntrneik2  38707  ntrneikb  38709  ntrneixb  38710  ntrneik3  38711  ntrneix3  38712  ntrneik13  38713  ntrneix13  38714  ntrneik4w  38715  ntrneik4  38716  clsneifv3  38725  clsneifv4  38726  neicvgfv  38736  k0004ss2  38767  k0004val0  38769  mapss2  39711  difmap  39713  inmap  39715  difmapsn  39718  ssmapsn  39722  mccllem  40147  dvnprodlem1  40479  dvnprodlem2  40480  fourierdlem11  40653  fourierdlem12  40654  fourierdlem13  40655  fourierdlem14  40656  fourierdlem34  40676  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem54  40695  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem69  40710  fourierdlem72  40713  fourierdlem74  40715  fourierdlem75  40716  fourierdlem79  40720  fourierdlem85  40726  fourierdlem88  40729  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem92  40733  fourierdlem94  40735  fourierdlem97  40738  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem113  40754  etransclem24  40793  etransclem26  40795  etransclem27  40796  etransclem28  40797  etransclem31  40800  etransclem32  40801  etransclem33  40802  etransclem34  40803  etransclem35  40804  etransclem37  40806  etransclem38  40807  rrxbasefi  40821  rrxdsfi  40823  rrxtopnfi  40824  rrndistlt  40828  qndenserrnbllem  40832  rrxsnicc  40838  ioorrnopnlem  40842  subsaliuncl  40894  hoicvr  41083  ovnprodcl  41089  ovnsupge0  41092  ovnlecvr  41093  ovncvrrp  41099  ovn0lem  41100  ovnsubaddlem1  41105  sge0hsphoire  41124  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  hoidmvlelem5  41134  hoidmvle  41135  ovnhoilem2  41137  ovnlecvr2  41145  ovncvr2  41146  hoiqssbllem1  41157  hoiqssbllem2  41158  hoiqssbllem3  41159  hspmbllem2  41162  opnvonmbllem2  41168  ovolval2lem  41178  ovolval2  41179  ovolval3  41182  ovolval4lem2  41185  ovolval5lem3  41189  ovnovollem1  41191  ovnovollem2  41192  vonvolmbllem  41195  vonvolmbl2  41198  vonvol2  41199  snvonmbl  41221  vonsn  41226  iccpartxr  41680  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  intop  42164  assintop  42170  isassintop  42171  ofaddmndmap  42447  rmsupp0  42474  domnmsuppn0  42475  rmsuppss  42476  mndpsuppss  42477  scmsuppss  42478  gsumlsscl  42489  lincfsuppcl  42527  linccl  42528  lcosn0  42534  lincdifsn  42538  lincsum  42543  lincscm  42544  lincscmcl  42546  islinindfis  42563  lincext1  42568  lincext2  42569  lincext3  42570  lindslinindimp2lem1  42572  lindslinindimp2lem2  42573  lindslinindimp2lem4  42575  lindslinindsimp2lem5  42576  snlindsntor  42585  lincresunitlem2  42590  lincresunit3lem1  42593  lincresunit3lem2  42594  lincresunit3  42595  lincreslvec3  42596  isldepslvec2  42599  zlmodzxzldeplem2  42615  zlmodzxzldeplem3  42616  ldepsnlinclem1  42619  ldepsnlinclem2  42620  aacllem  42875
  Copyright terms: Public domain W3C validator