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

Theorem elmapi 8124
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 8123 . . 3 (𝐴 ∈ (𝐵𝑚 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2 elmapg 8115 . . 3 ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵𝑚 𝐶) ↔ 𝐴:𝐶𝐵))
31, 2syl 17 . 2 (𝐴 ∈ (𝐵𝑚 𝐶) → (𝐴 ∈ (𝐵𝑚 𝐶) ↔ 𝐴:𝐶𝐵))
43ibi 258 1 (𝐴 ∈ (𝐵𝑚 𝐶) → 𝐴:𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wcel 2157  Vcvv 3402  wf 6107  (class class class)co 6884  𝑚 cmap 8102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5232  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-fv 6119  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-1st 7408  df-2nd 7409  df-map 8104
This theorem is referenced by:  elmapfn  8125  elmapfun  8126  elmapssres  8127  mapsspm  8136  map0b  8142  mapss  8147  mapsncnv  8151  ralxpmap  8154  mapen  8373  mapxpen  8375  mapunen  8378  mapfienlem1  8559  mapfienlem2  8560  mapfienlem3  8561  mapfien  8562  wemaplem2  8701  wemappo  8703  wemapsolem  8704  wemapso  8705  wemapso2lem  8706  wemapwe  8851  iunmapdisj  9139  fseqenlem1  9140  fseqenlem2  9141  numacn  9165  finacn  9166  acndom  9167  acndom2  9170  infpwfien  9178  infmap2  9335  fin23lem40  9468  isf32lem12  9481  isf34lem6  9497  acncc  9557  pwfseqlem3  9777  pwxpndom2  9782  ramval  15949  ramub  15954  ramcl  15970  prmgaplem7  15998  prmgaplem8  15999  imasdsval2  16401  funcf2  16752  funcpropd  16784  funcestrcsetclem8  17012  funcestrcsetclem9  17013  funcsetcestrclem8  17027  funcsetcestrclem9  17028  fsfnn0gsumfsffz  18600  gsummptnn0fzfv  18606  mplbas2  19699  ltbwe  19701  psr1baslem  19783  psr1basf  19799  fvcoe1  19805  coe1mul2lem1  19865  ply1coe  19894  frlmfibas  20336  frlmbas3  20346  frlmipval  20349  frlmphllem  20350  frlmphl  20351  elfilspd  20373  islindf4  20408  mamures  20427  mndvcl  20428  mndvass  20429  mndvlid  20430  mndvrid  20431  grpvlinv  20432  grpvrinv  20433  mhmvlin  20434  mamucl  20438  mamuass  20439  mamudi  20440  mamudir  20441  mamuvs1  20442  mamuvs2  20443  mamulid  20478  mamurid  20479  mattposcl  20491  mattpostpos  20492  tposmap  20495  mamutpos  20496  matgsumcl  20498  mavmulcl  20585  mavmulass  20587  mavmulsolcl  20589  marepvcl  20607  1marepvmarrepid  20613  mdetleib2  20626  mdetf  20633  mdetdiaglem  20636  mdetrlin  20640  mdetrsca  20641  mdetralt  20646  mdetunilem7  20656  mdetunilem9  20658  maducoeval2  20678  madutpos  20680  madugsum  20681  madurid  20682  cramerimplem1  20722  cramerimplem1OLD  20723  m2pmfzmap  20786  decpmatval  20804  pmatcollpw3lem  20822  pmatcollpw3fi1lem1  20825  pmatcollpw3fi1lem2  20826  pm2mp  20864  chfacfisf  20893  chfacfisfcpmat  20894  chfacfscmulgsum  20899  chfacfpmmulgsum  20903  chfacfpmmulgsum2  20904  cayhamlem1  20905  cpmadugsumlemF  20915  cpmadugsumfi  20916  cayhamlem2  20923  chcoeffeqlem  20924  cayleyhamilton1  20931  pnrmopn  21382  xkoptsub  21692  xkopt  21693  tmdgsum  22133  imasdsf1olem  22412  rrxnm  23414  rrxds  23416  rrxf  23419  rrxmvallem  23422  ehlbase  23429  ovolscalem2  23518  uniioombl  23593  tdeglem2  24058  plypf1  24205  ulmclm  24378  ulmcaulem  24385  ulmcau  24386  ulmss  24388  ulmbdd  24389  ulmcn  24390  ulmdvlem1  24391  ulmdvlem2  24392  ulmdvlem3  24393  mtest  24395  mtestbdd  24396  mbfulm  24397  iblulm  24398  itgulm  24399  itgulm2  24400  adjval2  29101  fmptco1f1o  29784  fcobijfs  29851  resf1o  29855  fpwrelmap  29858  smatrcl  30210  mbfmf  30665  elmbfmvol2  30677  eulerpartlemelr  30767  eulerpartlemf  30780  eulerpartlemt  30781  eulerpartgbij  30782  eulerpartlemgu  30787  eulerpartlemgh  30788  eulerpartlemgf  30789  eulerpartlemgs2  30790  reprf  31038  reprsuc  31041  vtsprod  31065  circlemethhgt  31069  tgoldbachgtd  31088  mrsubff1  31756  mrsub0  31758  mrsubf  31759  mrsubccat  31760  mrsubcn  31761  msubrn  31771  msubff  31772  msubf  31774  msubff1  31798  mclsind  31812  uncf  33720  curunc  33723  unccur  33724  matunitlindflem1  33737  matunitlindflem2  33738  poimirlem4  33745  poimirlem5  33746  poimirlem6  33747  poimirlem7  33748  poimirlem8  33749  poimirlem10  33751  poimirlem11  33752  poimirlem12  33753  poimirlem16  33757  poimirlem17  33758  poimirlem18  33759  poimirlem19  33760  poimirlem20  33761  poimirlem21  33762  poimirlem22  33763  poimirlem25  33766  poimirlem26  33767  poimirlem27  33768  poimirlem29  33770  poimirlem30  33771  poimirlem31  33772  poimirlem32  33773  poimir  33774  broucube  33775  mblfinlem3  33780  mblfinlem4  33781  ismblfin  33782  rrnmet  33958  rrndstprj1  33959  rrndstprj2  33960  rrncmslem  33961  rrnequiv  33964  mapco2g  37797  mapfzcons1  37800  mapfzcons2  37802  mzpcompact2lem  37834  eldiophb  37840  elmapresaun  37854  elmapresaunres2  37855  eq0rabdioph  37860  rexrabdioph  37878  eldioph4b  37895  diophren  37897  rmydioph  38100  rmxdioph  38102  expdiophlem2  38108  expdioph  38109  pw2f1o2val2  38126  wepwsolem  38131  pwfi2f1o  38185  rfovcnvf1od  38816  rfovcnvfvd  38819  fsovrfovd  38821  fsovcnvlem  38825  ntrk0kbimka  38855  neik0pk1imk0  38863  ntrclsfveq1  38876  ntrclsfveq2  38877  ntrclsfveq  38878  ntrclsss  38879  ntrclsiso  38883  ntrclsk2  38884  ntrclskb  38885  ntrclsk3  38886  ntrclsk13  38887  ntrclsk4  38888  ntrneifv3  38898  ntrneineine0lem  38899  ntrneineine1lem  38900  ntrneifv4  38901  ntrneiel2  38902  ntrneicls00  38905  ntrneicls11  38906  ntrneiiso  38907  ntrneik2  38908  ntrneikb  38910  ntrneixb  38911  ntrneik3  38912  ntrneix3  38913  ntrneik13  38914  ntrneix13  38915  ntrneik4w  38916  ntrneik4  38917  clsneifv3  38926  clsneifv4  38927  neicvgfv  38937  k0004ss2  38968  k0004val0  38970  mapss2  39902  difmap  39904  inmap  39906  difmapsn  39909  ssmapsn  39913  mccllem  40327  dvnprodlem1  40659  dvnprodlem2  40660  fourierdlem11  40832  fourierdlem12  40833  fourierdlem13  40834  fourierdlem14  40835  fourierdlem34  40855  fourierdlem41  40862  fourierdlem48  40868  fourierdlem49  40869  fourierdlem54  40874  fourierdlem63  40883  fourierdlem64  40884  fourierdlem65  40885  fourierdlem69  40889  fourierdlem72  40892  fourierdlem74  40894  fourierdlem75  40895  fourierdlem79  40899  fourierdlem85  40905  fourierdlem88  40908  fourierdlem89  40909  fourierdlem90  40910  fourierdlem91  40911  fourierdlem92  40912  fourierdlem94  40914  fourierdlem97  40917  fourierdlem103  40923  fourierdlem104  40924  fourierdlem111  40931  fourierdlem113  40933  etransclem24  40972  etransclem26  40974  etransclem27  40975  etransclem28  40976  etransclem31  40979  etransclem32  40980  etransclem33  40981  etransclem34  40982  etransclem35  40983  etransclem37  40985  etransclem38  40986  rrxbasefi  41000  rrxdsfi  41002  rrxtopnfi  41003  rrndistlt  41007  qndenserrnbllem  41011  rrxsnicc  41017  ioorrnopnlem  41021  subsaliuncl  41073  hoicvr  41262  ovnprodcl  41268  ovnsupge0  41271  ovnlecvr  41272  ovncvrrp  41278  ovn0lem  41279  ovnsubaddlem1  41284  sge0hsphoire  41303  hoidmv1le  41308  hoidmvlelem1  41309  hoidmvlelem2  41310  hoidmvlelem3  41311  hoidmvlelem4  41312  hoidmvlelem5  41313  hoidmvle  41314  ovnhoilem2  41316  ovnlecvr2  41324  ovncvr2  41325  hoiqssbllem1  41336  hoiqssbllem2  41337  hoiqssbllem3  41338  hspmbllem2  41341  opnvonmbllem2  41347  ovolval2lem  41357  ovolval2  41358  ovolval3  41361  ovolval4lem2  41364  ovolval5lem3  41368  ovnovollem1  41370  ovnovollem2  41371  vonvolmbllem  41374  vonvolmbl2  41377  vonvol2  41378  snvonmbl  41400  vonsn  41405  iccpartxr  41948  nnsum4primeseven  42281  nnsum4primesevenALTV  42282  intop  42425  assintop  42431  isassintop  42432  ofaddmndmap  42708  rmsupp0  42735  domnmsuppn0  42736  rmsuppss  42737  mndpsuppss  42738  scmsuppss  42739  gsumlsscl  42750  lincfsuppcl  42788  linccl  42789  lcosn0  42795  lincdifsn  42799  lincsum  42804  lincscm  42805  lincscmcl  42807  islinindfis  42824  lincext1  42829  lincext2  42830  lincext3  42831  lindslinindimp2lem1  42833  lindslinindimp2lem2  42834  lindslinindimp2lem4  42836  lindslinindsimp2lem5  42837  snlindsntor  42846  lincresunitlem2  42851  lincresunit3lem1  42854  lincresunit3lem2  42855  lincresunit3  42856  lincreslvec3  42857  isldepslvec2  42860  zlmodzxzldeplem2  42876  zlmodzxzldeplem3  42877  ldepsnlinclem1  42880  ldepsnlinclem2  42881  aacllem  43136
  Copyright terms: Public domain W3C validator