Theorem elmapi 8595

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

Step	Hyp	Ref	Expression
1		elmapex 8594	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8586	. . 3 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
4	3	ibi 266	1 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  Vcvv 3422  ⟶wf 6414  (class class class)co 7255   ↑_m cmap 8573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1st 7804  df-2nd 7805  df-map 8575

This theorem is referenced by:  mapfset  8596  elmapfn  8611  elmapfun  8612  elmapssres  8613  mapsspm  8622  mapfvd  8625  elmapresaun  8626  map0b  8629  mapss  8635  mapsncnv  8639  ralxpmap  8642  mapen  8877  mapxpen  8879  mapunen  8882  mapfienlem1  9094  mapfienlem2  9095  mapfienlem3  9096  mapfien  9097  wemaplem2  9236  wemappo  9238  wemapsolem  9239  wemapso  9240  wemapso2lem  9241  wemapwe  9385  iunmapdisj  9710  fseqenlem1  9711  fseqenlem2  9712  numacn  9736  finacn  9737  acndom  9738  acndom2  9741  infpwfien  9749  infmap2  9905  fin23lem40  10038  isf32lem12  10051  isf34lem6  10067  acncc  10127  pwfseqlem3  10347  pwxpndom2  10352  ramval  16637  ramub  16642  ramcl  16658  prmgaplem7  16686  prmgaplem8  16687  imasdsval2  17144  funcf2  17499  funcpropd  17532  funcestrcsetclem8  17780  funcestrcsetclem9  17781  funcsetcestrclem8  17795  funcsetcestrclem9  17796  fsfnn0gsumfsffz  19499  gsummptnn0fzfv  19503  frlmfibas  20879  frlmbas3  20893  frlmipval  20896  frlmphllem  20897  frlmphl  20898  elfilspd  20920  islindf4  20955  psrbagf  21031  mplbas2  21153  ltbwe  21155  psr1baslem  21266  psr1basf  21282  fvcoe1  21288  coe1mul2lem1  21348  ply1coe  21377  mamures  21449  mndvcl  21450  mndvass  21451  mndvlid  21452  mndvrid  21453  grpvlinv  21454  grpvrinv  21455  mhmvlin  21456  mamucl  21458  mamuass  21459  mamudi  21460  mamudir  21461  mamuvs1  21462  mamuvs2  21463  mamulid  21498  mamurid  21499  mattposcl  21510  mattpostpos  21511  tposmap  21514  mamutpos  21515  matgsumcl  21517  mavmulcl  21604  mavmulass  21606  mavmulsolcl  21608  marepvcl  21626  1marepvmarrepid  21632  mdetleib2  21645  mdetf  21652  mdetdiaglem  21655  mdetrlin  21659  mdetrsca  21660  mdetralt  21665  mdetunilem7  21675  mdetunilem9  21677  maducoeval2  21697  madutpos  21699  madugsum  21700  madurid  21701  cramerimplem1  21740  m2pmfzmap  21804  decpmatval  21822  pmatcollpw3lem  21840  pmatcollpw3fi1lem1  21843  pmatcollpw3fi1lem2  21844  pm2mp  21882  chfacfisf  21911  chfacfisfcpmat  21912  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmadugsumlemF  21933  cpmadugsumfi  21934  cayhamlem2  21941  chcoeffeqlem  21942  cayleyhamilton1  21949  pnrmopn  22402  xkoptsub  22713  xkopt  22714  tmdgsum  23154  imasdsf1olem  23434  rrxnm  24460  rrxds  24462  rrxf  24470  rrxmvallem  24473  rrxbasefi  24479  rrxdsfi  24480  ehlbase  24484  ovolscalem2  24583  uniioombl  24658  tdeglem2  25131  plypf1  25278  ulmclm  25451  ulmcaulem  25458  ulmcau  25459  ulmss  25461  ulmbdd  25462  ulmcn  25463  ulmdvlem1  25464  ulmdvlem2  25465  ulmdvlem3  25466  mtest  25468  mtestbdd  25469  mbfulm  25470  iblulm  25471  itgulm  25472  itgulm2  25473  adjval2  30154  fmptco1f1o  30869  fcobijfs  30960  resf1o  30967  fpwrelmap  30970  elrspunidl  31508  fply1  31569  fedgmullem1  31612  fedgmul  31614  extdg1id  31640  smatrcl  31648  mbfmf  32122  elmbfmvol2  32134  eulerpartlemelr  32224  eulerpartlemf  32237  eulerpartlemt  32238  eulerpartgbij  32239  eulerpartlemgu  32244  eulerpartlemgh  32245  eulerpartlemgf  32246  eulerpartlemgs2  32247  reprf  32492  reprsuc  32495  vtsprod  32519  circlemethhgt  32523  tgoldbachgtd  32542  satfv1lem  33224  satfvel  33274  satefvfmla0  33280  satefvfmla1  33287  prv1n  33293  mrsubff1  33376  mrsub0  33378  mrsubf  33379  mrsubccat  33380  mrsubcn  33381  msubrn  33391  msubff  33392  msubf  33394  msubff1  33418  mclsind  33432  uncf  35683  curunc  35686  unccur  35687  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  poimir  35737  broucube  35738  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  rrnmet  35914  rrndstprj1  35915  rrndstprj2  35916  rrncmslem  35917  rrnequiv  35920  evlsbagval  40198  fsuppind  40202  mhphf  40208  mapco2g  40452  mapfzcons1  40455  mapfzcons2  40457  mzpcompact2lem  40489  eldiophb  40495  elmapresaunres2  40509  eq0rabdioph  40514  rexrabdioph  40532  eldioph4b  40549  diophren  40551  rmydioph  40752  rmxdioph  40754  expdiophlem2  40760  expdioph  40761  pw2f1o2val2  40778  wepwsolem  40783  pwfi2f1o  40837  rfovcnvf1od  41501  rfovcnvfvd  41504  fsovrfovd  41506  fsovcnvlem  41510  ntrk0kbimka  41538  neik0pk1imk0  41546  ntrclsfveq1  41559  ntrclsfveq2  41560  ntrclsfveq  41561  ntrclsss  41562  ntrclsiso  41566  ntrclsk2  41567  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  ntrclsk4  41571  ntrneifv3  41581  ntrneineine0lem  41582  ntrneineine1lem  41583  ntrneifv4  41584  ntrneiel2  41585  ntrneicls00  41588  ntrneicls11  41589  ntrneiiso  41590  ntrneik2  41591  ntrneikb  41593  ntrneixb  41594  ntrneik3  41595  ntrneix3  41596  ntrneik13  41597  ntrneix13  41598  ntrneik4w  41599  ntrneik4  41600  clsneifv3  41609  clsneifv4  41610  neicvgfv  41620  k0004ss2  41651  k0004val0  41653  mnringbasefd  41722  mnugrud  41791  mapss2  42634  difmap  42636  inmap  42638  difmapsn  42641  ssmapsn  42645  mccllem  43028  dvnprodlem1  43377  dvnprodlem2  43378  fourierdlem11  43549  fourierdlem12  43550  fourierdlem13  43551  fourierdlem14  43552  fourierdlem34  43572  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem54  43591  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem69  43606  fourierdlem72  43609  fourierdlem74  43611  fourierdlem75  43612  fourierdlem79  43616  fourierdlem85  43622  fourierdlem88  43625  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem92  43629  fourierdlem94  43631  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem113  43650  etransclem24  43689  etransclem26  43691  etransclem27  43692  etransclem28  43693  etransclem31  43696  etransclem32  43697  etransclem33  43698  etransclem34  43699  etransclem35  43700  etransclem37  43702  etransclem38  43703  rrxtopnfi  43718  rrndistlt  43721  qndenserrnbllem  43725  rrxsnicc  43731  ioorrnopnlem  43735  subsaliuncl  43787  hoicvr  43976  ovnprodcl  43982  ovnsupge0  43985  ovnlecvr  43986  ovncvrrp  43992  ovn0lem  43993  ovnsubaddlem1  43998  sge0hsphoire  44017  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoidmvlelem5  44027  hoidmvle  44028  ovnhoilem2  44030  ovnlecvr2  44038  ovncvr2  44039  hoiqssbllem1  44050  hoiqssbllem2  44051  hoiqssbllem3  44052  hspmbllem2  44055  opnvonmbllem2  44061  ovolval2lem  44071  ovolval2  44072  ovolval3  44075  ovolval4lem2  44078  ovolval5lem3  44082  ovnovollem1  44084  ovnovollem2  44085  vonvolmbllem  44088  vonvolmbl2  44091  vonvol2  44092  snvonmbl  44114  vonsn  44119  iccpartxr  44759  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  intop  45285  assintop  45291  isassintop  45292  ofaddmndmap  45567  rmsupp0  45592  domnmsuppn0  45593  rmsuppss  45594  mndpsuppss  45595  scmsuppss  45596  gsumlsscl  45607  lincfsuppcl  45642  linccl  45643  lcosn0  45649  lincdifsn  45653  lincsum  45658  lincscm  45659  lincscmcl  45661  islinindfis  45678  lincext1  45683  lincext2  45684  lincext3  45685  lindslinindimp2lem1  45687  lindslinindimp2lem2  45688  lindslinindimp2lem4  45690  lindslinindsimp2lem5  45691  snlindsntor  45700  lincresunitlem2  45705  lincresunit3lem1  45708  lincresunit3lem2  45709  lincresunit3  45710  lincreslvec3  45711  isldepslvec2  45714  zlmodzxzldeplem2  45730  zlmodzxzldeplem3  45731  ldepsnlinclem1  45734  ldepsnlinclem2  45735  1arymaptf1  45876  1arymaptfo  45877  2arympt  45883  2arymaptf1  45887  2arymaptfo  45888  prelrrx2b  45948  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  aacllem  46391