Theorem elmapi 8907

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  Vcvv 3488  ⟶wf 6569  (class class class)co 7448   ↑_m cmap 8884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-map 8886

This theorem is referenced by:  mapfset  8908  elmapfn  8923  elmapfun  8924  elmapssres  8925  mapsspm  8934  mapfvd  8937  elmapresaun  8938  map0b  8941  mapss  8947  mapsncnv  8951  ralxpmap  8954  mapen  9207  mapxpen  9209  mapunen  9212  mapfienlem1  9474  mapfienlem2  9475  mapfienlem3  9476  mapfien  9477  wemaplem2  9616  wemappo  9618  wemapsolem  9619  wemapso  9620  wemapso2lem  9621  wemapwe  9766  iunmapdisj  10092  fseqenlem1  10093  fseqenlem2  10094  numacn  10118  finacn  10119  acndom  10120  acndom2  10123  infpwfien  10131  infmap2  10286  fin23lem40  10420  isf32lem12  10433  isf34lem6  10449  acncc  10509  pwfseqlem3  10729  pwxpndom2  10734  ramval  17055  ramub  17060  ramcl  17076  prmgaplem7  17104  prmgaplem8  17105  imasdsval2  17576  funcf2  17932  funcpropd  17967  funcestrcsetclem8  18216  funcestrcsetclem9  18217  funcsetcestrclem8  18231  funcsetcestrclem9  18232  mndvcl  18832  mndvass  18833  mndvlid  18834  mndvrid  18835  mhmvlin  18836  fsfnn0gsumfsffz  20025  gsummptnn0fzfv  20029  frlmfibas  21805  frlmbas3  21819  frlmipval  21822  frlmphllem  21823  frlmphl  21824  elfilspd  21846  islindf4  21881  psrbagf  21961  mplbas2  22083  ltbwe  22085  psr1baslem  22207  psr1basf  22224  fvcoe1  22230  coe1mul2lem1  22291  ply1coe  22323  mamures  22422  grpvlinv  22423  grpvrinv  22424  mamucl  22426  mamuass  22427  mamudi  22428  mamudir  22429  mamuvs1  22430  mamuvs2  22431  mamulid  22468  mamurid  22469  mattposcl  22480  mattpostpos  22481  tposmap  22484  mamutpos  22485  matgsumcl  22487  mavmulcl  22574  mavmulass  22576  mavmulsolcl  22578  marepvcl  22596  1marepvmarrepid  22602  mdetleib2  22615  mdetf  22622  mdetdiaglem  22625  mdetrlin  22629  mdetrsca  22630  mdetralt  22635  mdetunilem7  22645  mdetunilem9  22647  maducoeval2  22667  madutpos  22669  madugsum  22670  madurid  22671  cramerimplem1  22710  m2pmfzmap  22774  decpmatval  22792  pmatcollpw3lem  22810  pmatcollpw3fi1lem1  22813  pmatcollpw3fi1lem2  22814  pm2mp  22852  chfacfisf  22881  chfacfisfcpmat  22882  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  chfacfpmmulgsum2  22892  cayhamlem1  22893  cpmadugsumlemF  22903  cpmadugsumfi  22904  cayhamlem2  22911  chcoeffeqlem  22912  cayleyhamilton1  22919  pnrmopn  23372  xkoptsub  23683  xkopt  23684  tmdgsum  24124  imasdsf1olem  24404  rrxnm  25444  rrxds  25446  rrxf  25454  rrxmvallem  25457  rrxbasefi  25463  rrxdsfi  25464  ehlbase  25468  ovolscalem2  25568  uniioombl  25643  tdeglem2  26120  plypf1  26271  ulmclm  26448  ulmcaulem  26455  ulmcau  26456  ulmss  26458  ulmbdd  26459  ulmcn  26460  ulmdvlem1  26461  ulmdvlem2  26462  ulmdvlem3  26463  mtest  26465  mtestbdd  26466  mbfulm  26467  iblulm  26468  itgulm  26469  itgulm2  26470  adjval2  31923  fmptco1f1o  32652  fcobijfs  32737  resf1o  32744  fpwrelmap  32747  elrspunidl  33421  elrspunsn  33422  1arithidomlem2  33529  1arithidom  33530  fply1  33549  ply1degltdimlem  33635  fedgmullem1  33642  fedgmul  33644  extdg1id  33676  smatrcl  33742  mbfmf  34218  elmbfmvol2  34232  eulerpartlemelr  34322  eulerpartlemf  34335  eulerpartlemt  34336  eulerpartgbij  34337  eulerpartlemgu  34342  eulerpartlemgh  34343  eulerpartlemgf  34344  eulerpartlemgs2  34345  reprf  34589  reprsuc  34592  vtsprod  34616  circlemethhgt  34620  tgoldbachgtd  34639  satfv1lem  35330  satfvel  35380  satefvfmla0  35386  satefvfmla1  35393  prv1n  35399  mrsubff1  35482  mrsub0  35484  mrsubf  35485  mrsubccat  35486  mrsubcn  35487  msubrn  35497  msubff  35498  msubf  35500  msubff1  35524  mclsind  35538  uncf  37559  curunc  37562  unccur  37563  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  poimir  37613  broucube  37614  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  rrnmet  37789  rrndstprj1  37790  rrndstprj2  37791  rrncmslem  37792  rrnequiv  37795  aks6d1c2lem4  42084  mapcod  42238  evlsvvvallem  42516  evlsvvval  42518  evlselv  42542  fsuppind  42545  mhphf  42552  mapco2g  42670  mapfzcons1  42673  mapfzcons2  42675  mzpcompact2lem  42707  eldiophb  42713  elmapresaunres2  42727  eq0rabdioph  42732  rexrabdioph  42750  eldioph4b  42767  diophren  42769  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  expdioph  42980  pw2f1o2val2  42997  wepwsolem  42999  pwfi2f1o  43053  ofoafo  43318  ofoaid1  43320  ofoaid2  43321  ofoaass  43322  ofoacom  43323  rfovcnvf1od  43966  rfovcnvfvd  43969  fsovrfovd  43971  fsovcnvlem  43975  ntrk0kbimka  44001  neik0pk1imk0  44009  ntrclsfveq1  44022  ntrclsfveq2  44023  ntrclsfveq  44024  ntrclsss  44025  ntrclsiso  44029  ntrclsk2  44030  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  ntrclsk4  44034  ntrneifv3  44044  ntrneineine0lem  44045  ntrneineine1lem  44046  ntrneifv4  44047  ntrneiel2  44048  ntrneicls00  44051  ntrneicls11  44052  ntrneiiso  44053  ntrneik2  44054  ntrneikb  44056  ntrneixb  44057  ntrneik3  44058  ntrneix3  44059  ntrneik13  44060  ntrneix13  44061  ntrneik4w  44062  ntrneik4  44063  clsneifv3  44072  clsneifv4  44073  neicvgfv  44083  k0004ss2  44114  k0004val0  44116  mnringbasefd  44184  mnugrud  44253  mapss2  45112  difmap  45114  inmap  45116  difmapsn  45119  ssmapsn  45123  mccllem  45518  dvnprodlem1  45867  dvnprodlem2  45868  fourierdlem11  46039  fourierdlem12  46040  fourierdlem13  46041  fourierdlem14  46042  fourierdlem34  46062  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem54  46081  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem69  46096  fourierdlem72  46099  fourierdlem74  46101  fourierdlem75  46102  fourierdlem79  46106  fourierdlem85  46112  fourierdlem88  46115  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem92  46119  fourierdlem94  46121  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem113  46140  etransclem24  46179  etransclem26  46181  etransclem27  46182  etransclem28  46183  etransclem31  46186  etransclem32  46187  etransclem33  46188  etransclem34  46189  etransclem35  46190  etransclem37  46192  etransclem38  46193  rrxtopnfi  46208  rrndistlt  46211  qndenserrnbllem  46215  rrxsnicc  46221  ioorrnopnlem  46225  subsaliuncl  46279  hoicvr  46469  ovnprodcl  46475  ovnsupge0  46478  ovnlecvr  46479  ovncvrrp  46485  ovn0lem  46486  ovnsubaddlem1  46491  sge0hsphoire  46510  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoidmvlelem5  46520  hoidmvle  46521  ovnhoilem2  46523  ovnlecvr2  46531  ovncvr2  46532  hoiqssbllem1  46543  hoiqssbllem2  46544  hoiqssbllem3  46545  hspmbllem2  46548  opnvonmbllem2  46554  ovolval2lem  46564  ovolval2  46565  ovolval3  46568  ovolval4lem2  46571  ovolval5lem3  46575  ovnovollem1  46577  ovnovollem2  46578  vonvolmbllem  46581  vonvolmbl2  46584  vonvol2  46585  snvonmbl  46607  vonsn  46612  iccpartxr  47293  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  intop  47926  assintop  47932  isassintop  47933  ofaddmndmap  48068  rmsupp0  48093  domnmsuppn0  48094  rmsuppss  48095  mndpsuppss  48096  scmsuppss  48097  gsumlsscl  48108  lincfsuppcl  48142  linccl  48143  lcosn0  48149  lincdifsn  48153  lincsum  48158  lincscm  48159  lincscmcl  48161  islinindfis  48178  lincext1  48183  lincext2  48184  lincext3  48185  lindslinindimp2lem1  48187  lindslinindimp2lem2  48188  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  snlindsntor  48200  lincresunitlem2  48205  lincresunit3lem1  48208  lincresunit3lem2  48209  lincresunit3  48210  lincreslvec3  48211  isldepslvec2  48214  zlmodzxzldeplem2  48230  zlmodzxzldeplem3  48231  ldepsnlinclem1  48234  ldepsnlinclem2  48235  1arymaptf1  48376  1arymaptfo  48377  2arympt  48383  2arymaptf1  48387  2arymaptfo  48388  prelrrx2b  48448  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  aacllem  48895