Theorem elmapi 7765

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

Step	Hyp	Ref	Expression
1		elmapex 7764	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 7757	. . 3 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵 ↑𝑚 𝐶) ↔ 𝐴:𝐶⟶𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → (𝐴 ∈ (𝐵 ↑𝑚 𝐶) ↔ 𝐴:𝐶⟶𝐵))
4	3	ibi 255	1 ⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → 𝐴:𝐶⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  Vcvv 3173  ⟶wf 5800  (class class class)co 6549   ↑_𝑚 cmap 7744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746

This theorem is referenced by:  elmapfn  7766  elmapfun  7767  elmapssres  7768  mapsspm  7777  map0b  7782  mapss  7786  mapsncnv  7790  ralxpmap  7793  mapen  8009  mapxpen  8011  mapunen  8014  mapfienlem1  8193  mapfienlem2  8194  mapfienlem3  8195  mapfien  8196  wemaplem2  8335  wemappo  8337  wemapsolem  8338  wemapso  8339  wemapso2lem  8340  wemapwe  8477  iunmapdisj  8729  fseqenlem1  8730  fseqenlem2  8731  numacn  8755  finacn  8756  acndom  8757  acndom2  8760  infpwfien  8768  infmap2  8923  fin23lem40  9056  isf32lem12  9069  isf34lem6  9085  acncc  9145  pwfseqlem3  9361  pwxpndom2  9366  ramval  15550  ramub  15555  ramcl  15571  prmgaplem7  15599  prmgaplem8  15600  imasdsval2  15999  funcf2  16351  funcpropd  16383  funcestrcsetclem8  16610  funcestrcsetclem9  16611  funcsetcestrclem8  16625  funcsetcestrclem9  16626  fsfnn0gsumfsffz  18202  gsummptnn0fzfv  18207  mplbas2  19291  ltbwe  19293  psr1baslem  19376  psr1basf  19392  fvcoe1  19398  coe1mul2lem1  19458  ply1coe  19487  frlmfibas  19924  frlmbas3  19934  frlmipval  19937  frlmphllem  19938  frlmphl  19939  elfilspd  19961  islindf4  19996  mamures  20015  mndvcl  20016  mndvass  20017  mndvlid  20018  mndvrid  20019  grpvlinv  20020  grpvrinv  20021  mhmvlin  20022  mamucl  20026  mamuass  20027  mamudi  20028  mamudir  20029  mamuvs1  20030  mamuvs2  20031  mamulid  20066  mamurid  20067  mattposcl  20078  mattpostpos  20079  tposmap  20082  mamutpos  20083  matgsumcl  20085  mavmulcl  20172  mavmulass  20174  mavmulsolcl  20176  marepvcl  20194  1marepvmarrepid  20200  mdetleib2  20213  mdetf  20220  mdetdiaglem  20223  mdetrlin  20227  mdetrsca  20228  mdetralt  20233  mdetunilem7  20243  mdetunilem9  20245  maducoeval2  20265  madutpos  20267  madugsum  20268  madurid  20269  cramerimplem1  20308  m2pmfzmap  20371  decpmatval  20389  pmatcollpw3lem  20407  pmatcollpw3fi1lem1  20410  pmatcollpw3fi1lem2  20411  pm2mp  20449  chfacfisf  20478  chfacfisfcpmat  20479  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  chfacfpmmulgsum2  20489  cayhamlem1  20490  cpmadugsumlemF  20500  cpmadugsumfi  20501  cayhamlem2  20508  chcoeffeqlem  20509  cayleyhamilton1  20516  pnrmopn  20957  xkoptsub  21267  xkopt  21268  tmdgsum  21709  imasdsf1olem  21988  rrxnm  22987  rrxds  22989  rrxf  22992  rrxmvallem  22995  ehlbase  23002  ovolscalem2  23089  uniioombl  23163  tdeglem2  23625  plypf1  23772  ulmclm  23945  ulmcaulem  23952  ulmcau  23953  ulmss  23955  ulmbdd  23956  ulmcn  23957  ulmdvlem1  23958  ulmdvlem2  23959  ulmdvlem3  23960  mtest  23962  mtestbdd  23963  mbfulm  23964  iblulm  23965  itgulm  23966  itgulm2  23967  adjval2  28134  fcobijfs  28889  resf1o  28893  fpwrelmap  28896  smatrcl  29190  mbfmf  29644  elmbfmvol2  29656  eulerpartlemelr  29746  eulerpartlemf  29759  eulerpartlemt  29760  eulerpartgbij  29761  eulerpartlemgu  29766  eulerpartlemgh  29767  eulerpartlemgf  29768  eulerpartlemgs2  29769  mrsubff1  30665  mrsub0  30667  mrsubf  30668  mrsubccat  30669  mrsubcn  30670  msubrn  30680  msubff  30681  msubf  30683  msubff1  30707  mclsind  30721  uncf  32558  curunc  32561  unccur  32562  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  poimir  32612  broucube  32613  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  rrnmet  32798  rrndstprj1  32799  rrndstprj2  32800  rrncmslem  32801  rrnequiv  32804  mapco2g  36295  mapfzcons1  36298  mapfzcons2  36300  mzpcompact2lem  36332  eldiophb  36338  elmapresaun  36352  elmapresaunres2  36353  eq0rabdioph  36358  rexrabdioph  36376  eldioph4b  36393  diophren  36395  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  expdioph  36608  pw2f1o2val2  36625  wepwsolem  36630  pwfi2f1o  36684  rfovcnvf1od  37318  rfovcnvfvd  37321  fsovrfovd  37323  fsovcnvlem  37327  ntrk0kbimka  37357  neik0pk1imk0  37365  ntrclsfveq1  37378  ntrclsfveq2  37379  ntrclsfveq  37380  ntrclsss  37381  ntrclsiso  37385  ntrclsk2  37386  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  ntrclsk4  37390  ntrneifv3  37400  ntrneineine0lem  37401  ntrneineine1lem  37402  ntrneifv4  37403  ntrneiel2  37404  ntrneicls00  37407  ntrneicls11  37408  ntrneiiso  37409  ntrneik2  37410  ntrneikb  37412  ntrneixb  37413  ntrneik3  37414  ntrneix3  37415  ntrneik13  37416  ntrneix13  37417  ntrneik4w  37418  ntrneik4  37419  clsneifv3  37428  clsneifv4  37429  neicvgfv  37439  k0004ss2  37470  k0004val0  37472  mapss2  38392  difmap  38394  inmap  38396  difmapsn  38399  ssmapsn  38403  mccllem  38664  dvnprodlem1  38836  dvnprodlem2  38837  fourierdlem11  39011  fourierdlem12  39012  fourierdlem13  39013  fourierdlem14  39014  fourierdlem34  39034  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem54  39053  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem69  39068  fourierdlem72  39071  fourierdlem74  39073  fourierdlem75  39074  fourierdlem79  39078  fourierdlem85  39084  fourierdlem88  39087  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem94  39093  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem113  39112  etransclem24  39151  etransclem26  39153  etransclem27  39154  etransclem28  39155  etransclem31  39158  etransclem32  39159  etransclem33  39160  etransclem34  39161  etransclem35  39162  etransclem37  39164  etransclem38  39165  rrxbasefi  39179  rrxdsfi  39181  rrxtopnfi  39182  rrndistlt  39186  qndenserrnbllem  39190  rrxsnicc  39196  ioorrnopnlem  39200  subsaliuncl  39252  hoicvr  39438  ovnprodcl  39444  ovnsupge0  39447  ovnlecvr  39448  ovncvrrp  39454  ovn0lem  39455  ovnsubaddlem1  39460  sge0hsphoire  39479  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoidmvlelem5  39489  hoidmvle  39490  ovnhoilem2  39492  ovnlecvr2  39500  ovncvr2  39501  hoiqssbllem1  39512  hoiqssbllem2  39513  hoiqssbllem3  39514  hspmbllem2  39517  opnvonmbllem2  39523  ovolval2lem  39533  ovolval2  39534  ovolval3  39537  ovolval4lem2  39540  ovolval5lem3  39544  ovnovollem1  39546  ovnovollem2  39547  vonvolmbllem  39550  vonvolmbl2  39553  vonvol2  39554  snvonmbl  39577  vonsn  39582  iccpartxr  39957  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  intop  41629  assintop  41635  isassintop  41636  ofaddmndmap  41915  rmsupp0  41943  domnmsuppn0  41944  rmsuppss  41945  mndpsuppss  41946  scmsuppss  41947  gsumlsscl  41958  lincfsuppcl  41996  linccl  41997  lcosn0  42003  lincdifsn  42007  lincsum  42012  lincscm  42013  lincscmcl  42015  islinindfis  42032  lincext1  42037  lincext2  42038  lincext3  42039  lindslinindimp2lem1  42041  lindslinindimp2lem2  42042  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  snlindsntor  42054  lincresunitlem2  42059  lincresunit3lem1  42062  lincresunit3lem2  42063  lincresunit3  42064  lincreslvec3  42065  isldepslvec2  42068  zlmodzxzldeplem2  42084  zlmodzxzldeplem3  42085  ldepsnlinclem1  42088  ldepsnlinclem2  42089  aacllem  42356