Theorem elmapi 8824

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 8823	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8814	. . 3 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
4	3	ibi 269	1 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2141  Vcvv 3453  ⟶wf 6511  (class class class)co 7390   ↑_m cmap 8801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-fv 6523  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7964  df-2nd 7965  df-map 8803

This theorem is referenced by:  mapfset  8825  elmapfn  8840  elmapfun  8841  elmapssres  8842  mapsspm  8852  mapfvd  8855  elmapresaun  8856  map0b  8859  mapss  8865  mapsncnv  8869  ralxpmap  8872  mapen  9107  mapxpen  9109  mapunen  9112  mapfienlem1  9346  mapfienlem2  9347  mapfienlem3  9348  mapfien  9349  wemaplem2  9490  wemappo  9492  wemapsolem  9493  wemapso  9494  wemapso2lem  9495  wemapwe  9647  iunmapdisj  9974  fseqenlem1  9975  fseqenlem2  9976  numacn  10000  finacn  10001  acndom  10002  acndom2  10005  infpwfien  10013  infmap2  10168  fin23lem40  10303  isf32lem12  10316  isf34lem6  10332  acncc  10392  pwfseqlem3  10613  pwxpndom2  10618  ramval  17025  ramub  17030  ramcl  17046  prmgaplem7  17074  prmgaplem8  17075  imasdsval2  17527  funcf2  17882  funcpropd  17916  funcestrcsetclem8  18160  funcestrcsetclem9  18161  funcsetcestrclem8  18175  funcsetcestrclem9  18176  mndpsuppss  18780  mndvcl  18812  mndvass  18813  mndvlid  18814  mndvrid  18815  mhmvlin  18816  fsfnn0gsumfsffz  20004  gsummptnn0fzfv  20008  frlmfibas  21792  frlmbas3  21806  frlmipval  21809  frlmphllem  21810  frlmphl  21811  elfilspd  21833  islindf4  21868  psrbagf  21948  mplbas2  22073  ltbwe  22075  evlsvvvallem  22122  evlsvvval  22124  psr1baslem  22225  psr1basf  22241  fvcoe1  22247  coe1mul2lem1  22308  ply1coe  22339  mamures  22435  grpvlinv  22436  grpvrinv  22437  mamucl  22439  mamuass  22440  mamudi  22441  mamudir  22442  mamuvs1  22443  mamuvs2  22444  mamulid  22479  mamurid  22480  mattposcl  22491  mattpostpos  22492  tposmap  22495  mamutpos  22496  matgsumcl  22498  mavmulcl  22585  mavmulass  22587  mavmulsolcl  22589  marepvcl  22607  1marepvmarrepid  22613  mdetleib2  22626  mdetf  22633  mdetdiaglem  22636  mdetrlin  22640  mdetrsca  22641  mdetralt  22646  mdetunilem7  22656  mdetunilem9  22658  maducoeval2  22678  madutpos  22680  madugsum  22681  madurid  22682  cramerimplem1  22721  m2pmfzmap  22785  decpmatval  22803  pmatcollpw3lem  22821  pmatcollpw3fi1lem1  22824  pmatcollpw3fi1lem2  22825  pm2mp  22863  chfacfisf  22892  chfacfisfcpmat  22893  chfacfscmulgsum  22898  chfacfpmmulgsum  22902  chfacfpmmulgsum2  22903  cayhamlem1  22904  cpmadugsumlemF  22914  cpmadugsumfi  22915  cayhamlem2  22922  chcoeffeqlem  22923  cayleyhamilton1  22930  pnrmopn  23381  xkoptsub  23692  xkopt  23693  tmdgsum  24133  imasdsf1olem  24411  rrxnm  25431  rrxds  25433  rrxf  25441  rrxmvallem  25444  rrxbasefi  25450  rrxdsfi  25451  ehlbase  25455  ovolscalem2  25554  uniioombl  25629  tdeglem2  26099  plypf1  26250  ulmclm  26425  ulmcaulem  26432  ulmcau  26433  ulmss  26435  ulmbdd  26436  ulmcn  26437  ulmdvlem1  26438  ulmdvlem2  26439  ulmdvlem3  26440  mtest  26442  mtestbdd  26443  mbfulm  26444  iblulm  26445  itgulm  26446  itgulm2  26447  adjval2  32038  fmptco1f1o  32783  fcobijfs  32871  fcobijfs2  32872  resf1o  32880  fpwrelmap  32883  elrspunidl  33573  elrspunsn  33574  1arithidomlem2  33691  1arithidom  33692  fply1  33713  psrbasfsupp  33767  selvply1rhmlemb  33775  ply1degltdimlem  33878  fedgmullem1  33885  fedgmul  33887  extdg1id  33922  smatrcl  34052  mbfmf  34510  elmbfmvol2  34523  eulerpartlemelr  34613  eulerpartlemf  34626  eulerpartlemt  34627  eulerpartgbij  34628  eulerpartlemgu  34633  eulerpartlemgh  34634  eulerpartlemgf  34635  eulerpartlemgs2  34636  reprf  34868  reprsuc  34871  vtsprod  34895  circlemethhgt  34899  tgoldbachgtd  34918  satfv1lem  35665  satfvel  35715  satefvfmla0  35721  satefvfmla1  35728  prv1n  35734  mrsubff1  35817  mrsub0  35819  mrsubf  35820  mrsubccat  35821  mrsubcn  35822  msubrn  35832  msubff  35833  msubf  35835  msubff1  35859  mclsind  35873  uncf  38051  curunc  38054  unccur  38055  matunitlindflem1  38068  matunitlindflem2  38069  poimirlem4  38076  poimirlem5  38077  poimirlem6  38078  poimirlem7  38079  poimirlem8  38080  poimirlem10  38082  poimirlem11  38083  poimirlem12  38084  poimirlem16  38088  poimirlem17  38089  poimirlem18  38090  poimirlem19  38091  poimirlem20  38092  poimirlem21  38093  poimirlem22  38094  poimirlem25  38097  poimirlem26  38098  poimirlem27  38099  poimirlem29  38101  poimirlem30  38102  poimirlem31  38103  poimirlem32  38104  poimir  38105  broucube  38106  mblfinlem3  38111  mblfinlem4  38112  ismblfin  38113  rrnmet  38281  rrndstprj1  38282  rrndstprj2  38283  rrncmslem  38284  rrnequiv  38287  aks6d1c2lem4  42697  mapcod  42812  evlselv  43124  fsuppind  43125  mhphf  43132  mapco2g  43248  mapfzcons1  43251  mapfzcons2  43253  mzpcompact2lem  43285  eldiophb  43291  elmapresaunres2  43305  eq0rabdioph  43310  rexrabdioph  43324  eldioph4b  43341  diophren  43343  rmydioph  43544  rmxdioph  43546  expdiophlem2  43552  expdioph  43553  pw2f1o2val2  43570  wepwsolem  43572  pwfi2f1o  43626  ofoafo  43886  ofoaid1  43888  ofoaid2  43889  ofoaass  43890  ofoacom  43891  rfovcnvf1od  44533  rfovcnvfvd  44536  fsovrfovd  44538  fsovcnvlem  44542  ntrk0kbimka  44568  neik0pk1imk0  44576  ntrclsfveq1  44589  ntrclsfveq2  44590  ntrclsfveq  44591  ntrclsss  44592  ntrclsiso  44596  ntrclsk2  44597  ntrclskb  44598  ntrclsk3  44599  ntrclsk13  44600  ntrclsk4  44601  ntrneifv3  44611  ntrneineine0lem  44612  ntrneineine1lem  44613  ntrneifv4  44614  ntrneiel2  44615  ntrneicls00  44618  ntrneicls11  44619  ntrneiiso  44620  ntrneik2  44621  ntrneikb  44623  ntrneixb  44624  ntrneik3  44625  ntrneix3  44626  ntrneik13  44627  ntrneix13  44628  ntrneik4w  44629  ntrneik4  44630  clsneifv3  44639  clsneifv4  44640  neicvgfv  44650  k0004ss2  44681  k0004val0  44683  mnringbasefd  44747  mnugrud  44813  mapss2  45735  difmap  45736  inmap  45738  difmapsn  45741  ssmapsn  45745  mccllem  46126  dvnprodlem1  46473  dvnprodlem2  46474  fourierdlem11  46645  fourierdlem12  46646  fourierdlem13  46647  fourierdlem14  46648  fourierdlem34  46668  fourierdlem41  46675  fourierdlem48  46681  fourierdlem49  46682  fourierdlem54  46687  fourierdlem63  46696  fourierdlem64  46697  fourierdlem65  46698  fourierdlem69  46702  fourierdlem72  46705  fourierdlem74  46707  fourierdlem75  46708  fourierdlem79  46712  fourierdlem85  46718  fourierdlem88  46721  fourierdlem89  46722  fourierdlem90  46723  fourierdlem91  46724  fourierdlem92  46725  fourierdlem94  46727  fourierdlem97  46730  fourierdlem103  46736  fourierdlem104  46737  fourierdlem111  46744  fourierdlem113  46746  etransclem24  46785  etransclem26  46787  etransclem27  46788  etransclem28  46789  etransclem31  46792  etransclem32  46793  etransclem33  46794  etransclem34  46795  etransclem35  46796  etransclem37  46798  etransclem38  46799  rrxtopnfi  46814  rrndistlt  46817  qndenserrnbllem  46821  rrxsnicc  46827  ioorrnopnlem  46831  subsaliuncl  46885  hoicvr  47075  ovnprodcl  47081  ovnsupge0  47084  ovnlecvr  47085  ovncvrrp  47091  ovn0lem  47092  ovnsubaddlem1  47097  sge0hsphoire  47116  hoidmv1le  47121  hoidmvlelem1  47122  hoidmvlelem2  47123  hoidmvlelem3  47124  hoidmvlelem4  47125  hoidmvlelem5  47126  hoidmvle  47127  ovnhoilem2  47129  ovnlecvr2  47137  ovncvr2  47138  hoiqssbllem1  47149  hoiqssbllem2  47150  hoiqssbllem3  47151  hspmbllem2  47154  opnvonmbllem2  47160  ovolval2lem  47170  ovolval2  47171  ovolval3  47174  ovolval4lem2  47177  ovolval5lem3  47181  ovnovollem1  47183  ovnovollem2  47184  vonvolmbllem  47187  vonvolmbl2  47190  vonvol2  47191  snvonmbl  47213  vonsn  47218  iccpartxr  47978  nnsum4primeseven  48375  nnsum4primesevenALTV  48376  intop  48778  assintop  48784  isassintop  48785  ofaddmndmap  48918  rmsupp0  48943  domnmsuppn0  48944  rmsuppss  48945  scmsuppss  48946  gsumlsscl  48955  lincfsuppcl  48988  linccl  48989  lcosn0  48995  lincdifsn  48999  lincsum  49004  lincscm  49005  lincscmcl  49007  islinindfis  49024  lincext1  49029  lincext2  49030  lincext3  49031  lindslinindimp2lem1  49033  lindslinindimp2lem2  49034  lindslinindimp2lem4  49036  lindslinindsimp2lem5  49037  snlindsntor  49046  lincresunitlem2  49051  lincresunit3lem1  49054  lincresunit3lem2  49055  lincresunit3  49056  lincreslvec3  49057  isldepslvec2  49060  zlmodzxzldeplem2  49076  zlmodzxzldeplem3  49077  ldepsnlinclem1  49080  ldepsnlinclem2  49081  1arymaptf1  49217  1arymaptfo  49218  2arympt  49224  2arymaptf1  49228  2arymaptfo  49229  prelrrx2b  49289  eenglngeehlnmlem1  49312  eenglngeehlnmlem2  49313  aacllem  50375