Theorem elmapi 8887

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 8886	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8877	. . 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 2105  Vcvv 3477  ⟶wf 6558  (class class class)co 7430   ↑_m cmap 8864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-map 8866

This theorem is referenced by:  mapfset  8888  elmapfn  8903  elmapfun  8904  elmapssres  8905  mapsspm  8914  mapfvd  8917  elmapresaun  8918  map0b  8921  mapss  8927  mapsncnv  8931  ralxpmap  8934  mapen  9179  mapxpen  9181  mapunen  9184  mapfienlem1  9442  mapfienlem2  9443  mapfienlem3  9444  mapfien  9445  wemaplem2  9584  wemappo  9586  wemapsolem  9587  wemapso  9588  wemapso2lem  9589  wemapwe  9734  iunmapdisj  10060  fseqenlem1  10061  fseqenlem2  10062  numacn  10086  finacn  10087  acndom  10088  acndom2  10091  infpwfien  10099  infmap2  10254  fin23lem40  10388  isf32lem12  10401  isf34lem6  10417  acncc  10477  pwfseqlem3  10697  pwxpndom2  10702  ramval  17041  ramub  17046  ramcl  17062  prmgaplem7  17090  prmgaplem8  17091  imasdsval2  17562  funcf2  17918  funcpropd  17953  funcestrcsetclem8  18202  funcestrcsetclem9  18203  funcsetcestrclem8  18217  funcsetcestrclem9  18218  mndpsuppss  18790  mndvcl  18822  mndvass  18823  mndvlid  18824  mndvrid  18825  mhmvlin  18826  fsfnn0gsumfsffz  20015  gsummptnn0fzfv  20019  frlmfibas  21799  frlmbas3  21813  frlmipval  21816  frlmphllem  21817  frlmphl  21818  elfilspd  21840  islindf4  21875  psrbagf  21955  mplbas2  22077  ltbwe  22079  psr1baslem  22201  psr1basf  22218  fvcoe1  22224  coe1mul2lem1  22285  ply1coe  22317  mamures  22416  grpvlinv  22417  grpvrinv  22418  mamucl  22420  mamuass  22421  mamudi  22422  mamudir  22423  mamuvs1  22424  mamuvs2  22425  mamulid  22462  mamurid  22463  mattposcl  22474  mattpostpos  22475  tposmap  22478  mamutpos  22479  matgsumcl  22481  mavmulcl  22568  mavmulass  22570  mavmulsolcl  22572  marepvcl  22590  1marepvmarrepid  22596  mdetleib2  22609  mdetf  22616  mdetdiaglem  22619  mdetrlin  22623  mdetrsca  22624  mdetralt  22629  mdetunilem7  22639  mdetunilem9  22641  maducoeval2  22661  madutpos  22663  madugsum  22664  madurid  22665  cramerimplem1  22704  m2pmfzmap  22768  decpmatval  22786  pmatcollpw3lem  22804  pmatcollpw3fi1lem1  22807  pmatcollpw3fi1lem2  22808  pm2mp  22846  chfacfisf  22875  chfacfisfcpmat  22876  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  chfacfpmmulgsum2  22886  cayhamlem1  22887  cpmadugsumlemF  22897  cpmadugsumfi  22898  cayhamlem2  22905  chcoeffeqlem  22906  cayleyhamilton1  22913  pnrmopn  23366  xkoptsub  23677  xkopt  23678  tmdgsum  24118  imasdsf1olem  24398  rrxnm  25438  rrxds  25440  rrxf  25448  rrxmvallem  25451  rrxbasefi  25457  rrxdsfi  25458  ehlbase  25462  ovolscalem2  25562  uniioombl  25637  tdeglem2  26114  plypf1  26265  ulmclm  26444  ulmcaulem  26451  ulmcau  26452  ulmss  26454  ulmbdd  26455  ulmcn  26456  ulmdvlem1  26457  ulmdvlem2  26458  ulmdvlem3  26459  mtest  26461  mtestbdd  26462  mbfulm  26463  iblulm  26464  itgulm  26465  itgulm2  26466  adjval2  31919  fmptco1f1o  32649  fcobijfs  32740  resf1o  32747  fpwrelmap  32750  elrspunidl  33435  elrspunsn  33436  1arithidomlem2  33543  1arithidom  33544  fply1  33563  ply1degltdimlem  33649  fedgmullem1  33656  fedgmul  33658  extdg1id  33690  smatrcl  33756  mbfmf  34234  elmbfmvol2  34248  eulerpartlemelr  34338  eulerpartlemf  34351  eulerpartlemt  34352  eulerpartgbij  34353  eulerpartlemgu  34358  eulerpartlemgh  34359  eulerpartlemgf  34360  eulerpartlemgs2  34361  reprf  34605  reprsuc  34608  vtsprod  34632  circlemethhgt  34636  tgoldbachgtd  34655  satfv1lem  35346  satfvel  35396  satefvfmla0  35402  satefvfmla1  35409  prv1n  35415  mrsubff1  35498  mrsub0  35500  mrsubf  35501  mrsubccat  35502  mrsubcn  35503  msubrn  35513  msubff  35514  msubf  35516  msubff1  35540  mclsind  35554  uncf  37585  curunc  37588  unccur  37589  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  poimir  37639  broucube  37640  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  rrnmet  37815  rrndstprj1  37816  rrndstprj2  37817  rrncmslem  37818  rrnequiv  37821  aks6d1c2lem4  42108  mapcod  42262  evlsvvvallem  42547  evlsvvval  42549  evlselv  42573  fsuppind  42576  mhphf  42583  mapco2g  42701  mapfzcons1  42704  mapfzcons2  42706  mzpcompact2lem  42738  eldiophb  42744  elmapresaunres2  42758  eq0rabdioph  42763  rexrabdioph  42781  eldioph4b  42798  diophren  42800  rmydioph  43002  rmxdioph  43004  expdiophlem2  43010  expdioph  43011  pw2f1o2val2  43028  wepwsolem  43030  pwfi2f1o  43084  ofoafo  43345  ofoaid1  43347  ofoaid2  43348  ofoaass  43349  ofoacom  43350  rfovcnvf1od  43993  rfovcnvfvd  43996  fsovrfovd  43998  fsovcnvlem  44002  ntrk0kbimka  44028  neik0pk1imk0  44036  ntrclsfveq1  44049  ntrclsfveq2  44050  ntrclsfveq  44051  ntrclsss  44052  ntrclsiso  44056  ntrclsk2  44057  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrclsk4  44061  ntrneifv3  44071  ntrneineine0lem  44072  ntrneineine1lem  44073  ntrneifv4  44074  ntrneiel2  44075  ntrneicls00  44078  ntrneicls11  44079  ntrneiiso  44080  ntrneik2  44081  ntrneikb  44083  ntrneixb  44084  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  ntrneik4w  44089  ntrneik4  44090  clsneifv3  44099  clsneifv4  44100  neicvgfv  44110  k0004ss2  44141  k0004val0  44143  mnringbasefd  44210  mnugrud  44279  mapss2  45147  difmap  45149  inmap  45151  difmapsn  45154  ssmapsn  45158  mccllem  45552  dvnprodlem1  45901  dvnprodlem2  45902  fourierdlem11  46073  fourierdlem12  46074  fourierdlem13  46075  fourierdlem14  46076  fourierdlem34  46096  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem54  46115  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem69  46130  fourierdlem72  46133  fourierdlem74  46135  fourierdlem75  46136  fourierdlem79  46140  fourierdlem85  46146  fourierdlem88  46149  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem92  46153  fourierdlem94  46155  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem113  46174  etransclem24  46213  etransclem26  46215  etransclem27  46216  etransclem28  46217  etransclem31  46220  etransclem32  46221  etransclem33  46222  etransclem34  46223  etransclem35  46224  etransclem37  46226  etransclem38  46227  rrxtopnfi  46242  rrndistlt  46245  qndenserrnbllem  46249  rrxsnicc  46255  ioorrnopnlem  46259  subsaliuncl  46313  hoicvr  46503  ovnprodcl  46509  ovnsupge0  46512  ovnlecvr  46513  ovncvrrp  46519  ovn0lem  46520  ovnsubaddlem1  46525  sge0hsphoire  46544  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  hoidmvlelem5  46554  hoidmvle  46555  ovnhoilem2  46557  ovnlecvr2  46565  ovncvr2  46566  hoiqssbllem1  46577  hoiqssbllem2  46578  hoiqssbllem3  46579  hspmbllem2  46582  opnvonmbllem2  46588  ovolval2lem  46598  ovolval2  46599  ovolval3  46602  ovolval4lem2  46605  ovolval5lem3  46609  ovnovollem1  46611  ovnovollem2  46612  vonvolmbllem  46615  vonvolmbl2  46618  vonvol2  46619  snvonmbl  46641  vonsn  46646  iccpartxr  47343  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  intop  48046  assintop  48052  isassintop  48053  ofaddmndmap  48187  rmsupp0  48212  domnmsuppn0  48213  rmsuppss  48214  scmsuppss  48215  gsumlsscl  48224  lincfsuppcl  48258  linccl  48259  lcosn0  48265  lincdifsn  48269  lincsum  48274  lincscm  48275  lincscmcl  48277  islinindfis  48294  lincext1  48299  lincext2  48300  lincext3  48301  lindslinindimp2lem1  48303  lindslinindimp2lem2  48304  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  snlindsntor  48316  lincresunitlem2  48321  lincresunit3lem1  48324  lincresunit3lem2  48325  lincresunit3  48326  lincreslvec3  48327  isldepslvec2  48330  zlmodzxzldeplem2  48346  zlmodzxzldeplem3  48347  ldepsnlinclem1  48350  ldepsnlinclem2  48351  1arymaptf1  48491  1arymaptfo  48492  2arympt  48498  2arymaptf1  48502  2arymaptfo  48503  prelrrx2b  48563  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  aacllem  49031