Theorem elmapi 8849

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2105  Vcvv 3473  ⟶wf 6539  (class class class)co 7412   ↑_m cmap 8826

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7979  df-2nd 7980  df-map 8828

This theorem is referenced by:  mapfset  8850  elmapfn  8865  elmapfun  8866  elmapssres  8867  mapsspm  8876  mapfvd  8879  elmapresaun  8880  map0b  8883  mapss  8889  mapsncnv  8893  ralxpmap  8896  mapen  9147  mapxpen  9149  mapunen  9152  mapfienlem1  9406  mapfienlem2  9407  mapfienlem3  9408  mapfien  9409  wemaplem2  9548  wemappo  9550  wemapsolem  9551  wemapso  9552  wemapso2lem  9553  wemapwe  9698  iunmapdisj  10024  fseqenlem1  10025  fseqenlem2  10026  numacn  10050  finacn  10051  acndom  10052  acndom2  10055  infpwfien  10063  infmap2  10219  fin23lem40  10352  isf32lem12  10365  isf34lem6  10381  acncc  10441  pwfseqlem3  10661  pwxpndom2  10666  ramval  16948  ramub  16953  ramcl  16969  prmgaplem7  16997  prmgaplem8  16998  imasdsval2  17469  funcf2  17825  funcpropd  17860  funcestrcsetclem8  18109  funcestrcsetclem9  18110  funcsetcestrclem8  18124  funcsetcestrclem9  18125  fsfnn0gsumfsffz  19899  gsummptnn0fzfv  19903  frlmfibas  21627  frlmbas3  21641  frlmipval  21644  frlmphllem  21645  frlmphl  21646  elfilspd  21668  islindf4  21703  psrbagf  21781  mplbas2  21908  ltbwe  21910  psr1baslem  22028  psr1basf  22044  fvcoe1  22050  coe1mul2lem1  22109  ply1coe  22140  mamures  22212  mndvcl  22213  mndvass  22214  mndvlid  22215  mndvrid  22216  grpvlinv  22217  grpvrinv  22218  mhmvlin  22219  mamucl  22221  mamuass  22222  mamudi  22223  mamudir  22224  mamuvs1  22225  mamuvs2  22226  mamulid  22263  mamurid  22264  mattposcl  22275  mattpostpos  22276  tposmap  22279  mamutpos  22280  matgsumcl  22282  mavmulcl  22369  mavmulass  22371  mavmulsolcl  22373  marepvcl  22391  1marepvmarrepid  22397  mdetleib2  22410  mdetf  22417  mdetdiaglem  22420  mdetrlin  22424  mdetrsca  22425  mdetralt  22430  mdetunilem7  22440  mdetunilem9  22442  maducoeval2  22462  madutpos  22464  madugsum  22465  madurid  22466  cramerimplem1  22505  m2pmfzmap  22569  decpmatval  22587  pmatcollpw3lem  22605  pmatcollpw3fi1lem1  22608  pmatcollpw3fi1lem2  22609  pm2mp  22647  chfacfisf  22676  chfacfisfcpmat  22677  chfacfscmulgsum  22682  chfacfpmmulgsum  22686  chfacfpmmulgsum2  22687  cayhamlem1  22688  cpmadugsumlemF  22698  cpmadugsumfi  22699  cayhamlem2  22706  chcoeffeqlem  22707  cayleyhamilton1  22714  pnrmopn  23167  xkoptsub  23478  xkopt  23479  tmdgsum  23919  imasdsf1olem  24199  rrxnm  25239  rrxds  25241  rrxf  25249  rrxmvallem  25252  rrxbasefi  25258  rrxdsfi  25259  ehlbase  25263  ovolscalem2  25363  uniioombl  25438  tdeglem2  25917  plypf1  26064  ulmclm  26238  ulmcaulem  26245  ulmcau  26246  ulmss  26248  ulmbdd  26249  ulmcn  26250  ulmdvlem1  26251  ulmdvlem2  26252  ulmdvlem3  26253  mtest  26255  mtestbdd  26256  mbfulm  26257  iblulm  26258  itgulm  26259  itgulm2  26260  adjval2  31577  fmptco1f1o  32290  fcobijfs  32381  resf1o  32388  fpwrelmap  32391  elrspunidl  32986  elrspunsn  32987  fply1  33077  ply1degltdimlem  33161  fedgmullem1  33168  fedgmul  33170  extdg1id  33196  smatrcl  33240  mbfmf  33716  elmbfmvol2  33730  eulerpartlemelr  33820  eulerpartlemf  33833  eulerpartlemt  33834  eulerpartgbij  33835  eulerpartlemgu  33840  eulerpartlemgh  33841  eulerpartlemgf  33842  eulerpartlemgs2  33843  reprf  34088  reprsuc  34091  vtsprod  34115  circlemethhgt  34119  tgoldbachgtd  34138  satfv1lem  34817  satfvel  34867  satefvfmla0  34873  satefvfmla1  34880  prv1n  34886  mrsubff1  34969  mrsub0  34971  mrsubf  34972  mrsubccat  34973  mrsubcn  34974  msubrn  34984  msubff  34985  msubf  34987  msubff1  35011  mclsind  35025  uncf  36931  curunc  36934  unccur  36935  matunitlindflem1  36948  matunitlindflem2  36949  poimirlem4  36956  poimirlem5  36957  poimirlem6  36958  poimirlem7  36959  poimirlem8  36960  poimirlem10  36962  poimirlem11  36963  poimirlem12  36964  poimirlem16  36968  poimirlem17  36969  poimirlem18  36970  poimirlem19  36971  poimirlem20  36972  poimirlem21  36973  poimirlem22  36974  poimirlem25  36977  poimirlem26  36978  poimirlem27  36979  poimirlem29  36981  poimirlem30  36982  poimirlem31  36983  poimirlem32  36984  poimir  36985  broucube  36986  mblfinlem3  36991  mblfinlem4  36992  ismblfin  36993  rrnmet  37161  rrndstprj1  37162  rrndstprj2  37163  rrncmslem  37164  rrnequiv  37167  mapcod  41534  evlsvvvallem  41596  evlsvvval  41598  evlselv  41622  fsuppind  41625  mhphf  41632  mapco2g  41915  mapfzcons1  41918  mapfzcons2  41920  mzpcompact2lem  41952  eldiophb  41958  elmapresaunres2  41972  eq0rabdioph  41977  rexrabdioph  41995  eldioph4b  42012  diophren  42014  rmydioph  42216  rmxdioph  42218  expdiophlem2  42224  expdioph  42225  pw2f1o2val2  42242  wepwsolem  42247  pwfi2f1o  42301  ofoafo  42569  ofoaid1  42571  ofoaid2  42572  ofoaass  42573  ofoacom  42574  rfovcnvf1od  43218  rfovcnvfvd  43221  fsovrfovd  43223  fsovcnvlem  43227  ntrk0kbimka  43253  neik0pk1imk0  43261  ntrclsfveq1  43274  ntrclsfveq2  43275  ntrclsfveq  43276  ntrclsss  43277  ntrclsiso  43281  ntrclsk2  43282  ntrclskb  43283  ntrclsk3  43284  ntrclsk13  43285  ntrclsk4  43286  ntrneifv3  43296  ntrneineine0lem  43297  ntrneineine1lem  43298  ntrneifv4  43299  ntrneiel2  43300  ntrneicls00  43303  ntrneicls11  43304  ntrneiiso  43305  ntrneik2  43306  ntrneikb  43308  ntrneixb  43309  ntrneik3  43310  ntrneix3  43311  ntrneik13  43312  ntrneix13  43313  ntrneik4w  43314  ntrneik4  43315  clsneifv3  43324  clsneifv4  43325  neicvgfv  43335  k0004ss2  43366  k0004val0  43368  mnringbasefd  43437  mnugrud  43506  mapss2  44363  difmap  44365  inmap  44367  difmapsn  44370  ssmapsn  44374  mccllem  44772  dvnprodlem1  45121  dvnprodlem2  45122  fourierdlem11  45293  fourierdlem12  45294  fourierdlem13  45295  fourierdlem14  45296  fourierdlem34  45316  fourierdlem41  45323  fourierdlem48  45329  fourierdlem49  45330  fourierdlem54  45335  fourierdlem63  45344  fourierdlem64  45345  fourierdlem65  45346  fourierdlem69  45350  fourierdlem72  45353  fourierdlem74  45355  fourierdlem75  45356  fourierdlem79  45360  fourierdlem85  45366  fourierdlem88  45369  fourierdlem89  45370  fourierdlem90  45371  fourierdlem91  45372  fourierdlem92  45373  fourierdlem94  45375  fourierdlem97  45378  fourierdlem103  45384  fourierdlem104  45385  fourierdlem111  45392  fourierdlem113  45394  etransclem24  45433  etransclem26  45435  etransclem27  45436  etransclem28  45437  etransclem31  45440  etransclem32  45441  etransclem33  45442  etransclem34  45443  etransclem35  45444  etransclem37  45446  etransclem38  45447  rrxtopnfi  45462  rrndistlt  45465  qndenserrnbllem  45469  rrxsnicc  45475  ioorrnopnlem  45479  subsaliuncl  45533  hoicvr  45723  ovnprodcl  45729  ovnsupge0  45732  ovnlecvr  45733  ovncvrrp  45739  ovn0lem  45740  ovnsubaddlem1  45745  sge0hsphoire  45764  hoidmv1le  45769  hoidmvlelem1  45770  hoidmvlelem2  45771  hoidmvlelem3  45772  hoidmvlelem4  45773  hoidmvlelem5  45774  hoidmvle  45775  ovnhoilem2  45777  ovnlecvr2  45785  ovncvr2  45786  hoiqssbllem1  45797  hoiqssbllem2  45798  hoiqssbllem3  45799  hspmbllem2  45802  opnvonmbllem2  45808  ovolval2lem  45818  ovolval2  45819  ovolval3  45822  ovolval4lem2  45825  ovolval5lem3  45829  ovnovollem1  45831  ovnovollem2  45832  vonvolmbllem  45835  vonvolmbl2  45838  vonvol2  45839  snvonmbl  45861  vonsn  45866  iccpartxr  46546  nnsum4primeseven  46927  nnsum4primesevenALTV  46928  intop  47040  assintop  47046  isassintop  47047  ofaddmndmap  47182  rmsupp0  47207  domnmsuppn0  47208  rmsuppss  47209  mndpsuppss  47210  scmsuppss  47211  gsumlsscl  47222  lincfsuppcl  47256  linccl  47257  lcosn0  47263  lincdifsn  47267  lincsum  47272  lincscm  47273  lincscmcl  47275  islinindfis  47292  lincext1  47297  lincext2  47298  lincext3  47299  lindslinindimp2lem1  47301  lindslinindimp2lem2  47302  lindslinindimp2lem4  47304  lindslinindsimp2lem5  47305  snlindsntor  47314  lincresunitlem2  47319  lincresunit3lem1  47322  lincresunit3lem2  47323  lincresunit3  47324  lincreslvec3  47325  isldepslvec2  47328  zlmodzxzldeplem2  47344  zlmodzxzldeplem3  47345  ldepsnlinclem1  47348  ldepsnlinclem2  47349  1arymaptf1  47490  1arymaptfo  47491  2arympt  47497  2arymaptf1  47501  2arymaptfo  47502  prelrrx2b  47562  eenglngeehlnmlem1  47585  eenglngeehlnmlem2  47586  aacllem  48010