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

Theorem elmapi 8787
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 (𝐴 ∈ (𝐵m 𝐶) → 𝐴:𝐶𝐵)

Proof of Theorem elmapi
StepHypRef Expression
1 elmapex 8786 . . 3 (𝐴 ∈ (𝐵m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2 elmapg 8778 . . 3 ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵m 𝐶) ↔ 𝐴:𝐶𝐵))
31, 2syl 17 . 2 (𝐴 ∈ (𝐵m 𝐶) → (𝐴 ∈ (𝐵m 𝐶) ↔ 𝐴:𝐶𝐵))
43ibi 266 1 (𝐴 ∈ (𝐵m 𝐶) → 𝐴:𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wcel 2106  Vcvv 3445  wf 6492  (class class class)co 7357  m cmap 8765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-map 8767
This theorem is referenced by:  mapfset  8788  elmapfn  8803  elmapfun  8804  elmapssres  8805  mapsspm  8814  mapfvd  8817  elmapresaun  8818  map0b  8821  mapss  8827  mapsncnv  8831  ralxpmap  8834  mapen  9085  mapxpen  9087  mapunen  9090  mapfienlem1  9341  mapfienlem2  9342  mapfienlem3  9343  mapfien  9344  wemaplem2  9483  wemappo  9485  wemapsolem  9486  wemapso  9487  wemapso2lem  9488  wemapwe  9633  iunmapdisj  9959  fseqenlem1  9960  fseqenlem2  9961  numacn  9985  finacn  9986  acndom  9987  acndom2  9990  infpwfien  9998  infmap2  10154  fin23lem40  10287  isf32lem12  10300  isf34lem6  10316  acncc  10376  pwfseqlem3  10596  pwxpndom2  10601  ramval  16880  ramub  16885  ramcl  16901  prmgaplem7  16929  prmgaplem8  16930  imasdsval2  17398  funcf2  17754  funcpropd  17787  funcestrcsetclem8  18035  funcestrcsetclem9  18036  funcsetcestrclem8  18050  funcsetcestrclem9  18051  fsfnn0gsumfsffz  19760  gsummptnn0fzfv  19764  frlmfibas  21168  frlmbas3  21182  frlmipval  21185  frlmphllem  21186  frlmphl  21187  elfilspd  21209  islindf4  21244  psrbagf  21320  mplbas2  21443  ltbwe  21445  psr1baslem  21556  psr1basf  21572  fvcoe1  21578  coe1mul2lem1  21638  ply1coe  21667  mamures  21739  mndvcl  21740  mndvass  21741  mndvlid  21742  mndvrid  21743  grpvlinv  21744  grpvrinv  21745  mhmvlin  21746  mamucl  21748  mamuass  21749  mamudi  21750  mamudir  21751  mamuvs1  21752  mamuvs2  21753  mamulid  21790  mamurid  21791  mattposcl  21802  mattpostpos  21803  tposmap  21806  mamutpos  21807  matgsumcl  21809  mavmulcl  21896  mavmulass  21898  mavmulsolcl  21900  marepvcl  21918  1marepvmarrepid  21924  mdetleib2  21937  mdetf  21944  mdetdiaglem  21947  mdetrlin  21951  mdetrsca  21952  mdetralt  21957  mdetunilem7  21967  mdetunilem9  21969  maducoeval2  21989  madutpos  21991  madugsum  21992  madurid  21993  cramerimplem1  22032  m2pmfzmap  22096  decpmatval  22114  pmatcollpw3lem  22132  pmatcollpw3fi1lem1  22135  pmatcollpw3fi1lem2  22136  pm2mp  22174  chfacfisf  22203  chfacfisfcpmat  22204  chfacfscmulgsum  22209  chfacfpmmulgsum  22213  chfacfpmmulgsum2  22214  cayhamlem1  22215  cpmadugsumlemF  22225  cpmadugsumfi  22226  cayhamlem2  22233  chcoeffeqlem  22234  cayleyhamilton1  22241  pnrmopn  22694  xkoptsub  23005  xkopt  23006  tmdgsum  23446  imasdsf1olem  23726  rrxnm  24755  rrxds  24757  rrxf  24765  rrxmvallem  24768  rrxbasefi  24774  rrxdsfi  24775  ehlbase  24779  ovolscalem2  24878  uniioombl  24953  tdeglem2  25426  plypf1  25573  ulmclm  25746  ulmcaulem  25753  ulmcau  25754  ulmss  25756  ulmbdd  25757  ulmcn  25758  ulmdvlem1  25759  ulmdvlem2  25760  ulmdvlem3  25761  mtest  25763  mtestbdd  25764  mbfulm  25765  iblulm  25766  itgulm  25767  itgulm2  25768  adjval2  30833  fmptco1f1o  31547  fcobijfs  31640  resf1o  31647  fpwrelmap  31650  elrspunidl  32203  fply1  32265  fedgmullem1  32324  fedgmul  32326  extdg1id  32352  smatrcl  32377  mbfmf  32853  elmbfmvol2  32867  eulerpartlemelr  32957  eulerpartlemf  32970  eulerpartlemt  32971  eulerpartgbij  32972  eulerpartlemgu  32977  eulerpartlemgh  32978  eulerpartlemgf  32979  eulerpartlemgs2  32980  reprf  33225  reprsuc  33228  vtsprod  33252  circlemethhgt  33256  tgoldbachgtd  33275  satfv1lem  33956  satfvel  34006  satefvfmla0  34012  satefvfmla1  34019  prv1n  34025  mrsubff1  34108  mrsub0  34110  mrsubf  34111  mrsubccat  34112  mrsubcn  34113  msubrn  34123  msubff  34124  msubf  34126  msubff1  34150  mclsind  34164  uncf  36057  curunc  36060  unccur  36061  matunitlindflem1  36074  matunitlindflem2  36075  poimirlem4  36082  poimirlem5  36083  poimirlem6  36084  poimirlem7  36085  poimirlem8  36086  poimirlem10  36088  poimirlem11  36089  poimirlem12  36090  poimirlem16  36094  poimirlem17  36095  poimirlem18  36096  poimirlem19  36097  poimirlem20  36098  poimirlem21  36099  poimirlem22  36100  poimirlem25  36103  poimirlem26  36104  poimirlem27  36105  poimirlem29  36107  poimirlem30  36108  poimirlem31  36109  poimirlem32  36110  poimir  36111  broucube  36112  mblfinlem3  36117  mblfinlem4  36118  ismblfin  36119  rrnmet  36288  rrndstprj1  36289  rrndstprj2  36290  rrncmslem  36291  rrnequiv  36294  evlsbagval  40736  fsuppind  40751  mhphf  40757  mapco2g  41023  mapfzcons1  41026  mapfzcons2  41028  mzpcompact2lem  41060  eldiophb  41066  elmapresaunres2  41080  eq0rabdioph  41085  rexrabdioph  41103  eldioph4b  41120  diophren  41122  rmydioph  41324  rmxdioph  41326  expdiophlem2  41332  expdioph  41333  pw2f1o2val2  41350  wepwsolem  41355  pwfi2f1o  41409  ofoafo  41656  ofoaid1  41658  ofoaid2  41659  ofoaass  41660  ofoacom  41661  rfovcnvf1od  42266  rfovcnvfvd  42269  fsovrfovd  42271  fsovcnvlem  42275  ntrk0kbimka  42301  neik0pk1imk0  42309  ntrclsfveq1  42322  ntrclsfveq2  42323  ntrclsfveq  42324  ntrclsss  42325  ntrclsiso  42329  ntrclsk2  42330  ntrclskb  42331  ntrclsk3  42332  ntrclsk13  42333  ntrclsk4  42334  ntrneifv3  42344  ntrneineine0lem  42345  ntrneineine1lem  42346  ntrneifv4  42347  ntrneiel2  42348  ntrneicls00  42351  ntrneicls11  42352  ntrneiiso  42353  ntrneik2  42354  ntrneikb  42356  ntrneixb  42357  ntrneik3  42358  ntrneix3  42359  ntrneik13  42360  ntrneix13  42361  ntrneik4w  42362  ntrneik4  42363  clsneifv3  42372  clsneifv4  42373  neicvgfv  42383  k0004ss2  42414  k0004val0  42416  mnringbasefd  42485  mnugrud  42554  mapss2  43416  difmap  43418  inmap  43420  difmapsn  43423  ssmapsn  43427  mccllem  43828  dvnprodlem1  44177  dvnprodlem2  44178  fourierdlem11  44349  fourierdlem12  44350  fourierdlem13  44351  fourierdlem14  44352  fourierdlem34  44372  fourierdlem41  44379  fourierdlem48  44385  fourierdlem49  44386  fourierdlem54  44391  fourierdlem63  44400  fourierdlem64  44401  fourierdlem65  44402  fourierdlem69  44406  fourierdlem72  44409  fourierdlem74  44411  fourierdlem75  44412  fourierdlem79  44416  fourierdlem85  44422  fourierdlem88  44425  fourierdlem89  44426  fourierdlem90  44427  fourierdlem91  44428  fourierdlem92  44429  fourierdlem94  44431  fourierdlem97  44434  fourierdlem103  44440  fourierdlem104  44441  fourierdlem111  44448  fourierdlem113  44450  etransclem24  44489  etransclem26  44491  etransclem27  44492  etransclem28  44493  etransclem31  44496  etransclem32  44497  etransclem33  44498  etransclem34  44499  etransclem35  44500  etransclem37  44502  etransclem38  44503  rrxtopnfi  44518  rrndistlt  44521  qndenserrnbllem  44525  rrxsnicc  44531  ioorrnopnlem  44535  subsaliuncl  44589  hoicvr  44779  ovnprodcl  44785  ovnsupge0  44788  ovnlecvr  44789  ovncvrrp  44795  ovn0lem  44796  ovnsubaddlem1  44801  sge0hsphoire  44820  hoidmv1le  44825  hoidmvlelem1  44826  hoidmvlelem2  44827  hoidmvlelem3  44828  hoidmvlelem4  44829  hoidmvlelem5  44830  hoidmvle  44831  ovnhoilem2  44833  ovnlecvr2  44841  ovncvr2  44842  hoiqssbllem1  44853  hoiqssbllem2  44854  hoiqssbllem3  44855  hspmbllem2  44858  opnvonmbllem2  44864  ovolval2lem  44874  ovolval2  44875  ovolval3  44878  ovolval4lem2  44881  ovolval5lem3  44885  ovnovollem1  44887  ovnovollem2  44888  vonvolmbllem  44891  vonvolmbl2  44894  vonvol2  44895  snvonmbl  44917  vonsn  44922  iccpartxr  45601  nnsum4primeseven  45982  nnsum4primesevenALTV  45983  intop  46127  assintop  46133  isassintop  46134  ofaddmndmap  46409  rmsupp0  46434  domnmsuppn0  46435  rmsuppss  46436  mndpsuppss  46437  scmsuppss  46438  gsumlsscl  46449  lincfsuppcl  46484  linccl  46485  lcosn0  46491  lincdifsn  46495  lincsum  46500  lincscm  46501  lincscmcl  46503  islinindfis  46520  lincext1  46525  lincext2  46526  lincext3  46527  lindslinindimp2lem1  46529  lindslinindimp2lem2  46530  lindslinindimp2lem4  46532  lindslinindsimp2lem5  46533  snlindsntor  46542  lincresunitlem2  46547  lincresunit3lem1  46550  lincresunit3lem2  46551  lincresunit3  46552  lincreslvec3  46553  isldepslvec2  46556  zlmodzxzldeplem2  46572  zlmodzxzldeplem3  46573  ldepsnlinclem1  46576  ldepsnlinclem2  46577  1arymaptf1  46718  1arymaptfo  46719  2arympt  46725  2arymaptf1  46729  2arymaptfo  46730  prelrrx2b  46790  eenglngeehlnmlem1  46813  eenglngeehlnmlem2  46814  aacllem  47238
  Copyright terms: Public domain W3C validator