Theorem elmapi 8853

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  Vcvv 3451  ⟶wf 6527  (class class class)co 7412   ↑_m cmap 8831

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7990  df-2nd 7991  df-map 8833

This theorem is used by:  elmaprd  8854  mapfset  8856  elmapfn  8871  elmapfun  8872  uncf  8875  elmapssres  8878  mapsspm  8888  mapfvd  8891  elmapresaun  8892  map0b  8895  mapss  8901  mapsncnv  8905  ralxpmap  8908  mapen  9144  mapxpen  9146  mapunen  9149  mapfienlem1  9381  mapfienlem2  9382  mapfienlem3  9383  mapfien  9384  wemaplem2  9525  wemappo  9527  wemapsolem  9528  wemapso  9529  wemapso2lem  9530  wemapwe  9682  iunmapdisj  10083  fseqenlem1  10084  fseqenlem2  10085  numacn  10109  finacn  10110  acndom  10111  acndom2  10114  infpwfien  10122  infmap2  10276  fin23lem40  10410  isf32lem12  10423  isf34lem6  10439  acncc  10499  pwfseqlem3  10726  pwxpndom2  10731  s3rex  15081  ramval  17166  ramub  17171  ramcl  17187  prmgaplem7  17215  prmgaplem8  17216  imasdsval2  17668  funcf2  18023  funcpropd  18057  funcestrcsetclem8  18301  funcestrcsetclem9  18302  funcsetcestrclem8  18316  funcsetcestrclem9  18317  mndpsuppss  18939  mndvcl  18972  mndvass  18973  mndvlid  18974  mndvrid  18975  mhmvlin  18976  fsfnn0gsumfsffz  20177  gsummptnn0fzfv  20181  frlmfibas  22048  frlmbas3  22062  frlmipval  22065  frlmphllem  22066  frlmphl  22067  elfilspd  22089  islindf4  22124  psrbagf  22206  mplbas2  22331  ltbwe  22333  evlsvvvallem  22380  evlsvvval  22382  psr1baslem  22483  psr1basf  22499  fvcoe1  22505  coe1mul2lem1  22566  ply1coe  22596  mamures  22692  grpvlinv  22693  grpvrinv  22694  mamucl  22696  mamuass  22697  mamudi  22698  mamudir  22699  mamuvs1  22700  mamuvs2  22701  mamulid  22736  mamurid  22737  mattposcl  22748  mattpostpos  22749  tposmap  22752  mamutpos  22753  matgsumcl  22755  mavmulcl  22842  mavmulass  22844  mavmulsolcl  22846  marepvcl  22864  1marepvmarrepid  22870  mdetleib2  22883  mdetf  22890  mdetdiaglem  22893  mdetrlin  22897  mdetrsca  22898  mdetralt  22903  mdetunilem7  22913  mdetunilem9  22915  maducoeval2  22935  madutpos  22937  madugsum  22938  madurid  22939  matunitlindflem1  22974  matunitlindflem2  22975  cramerimplem1  22981  m2pmfzmap  23045  decpmatval  23063  pmatcollpw3lem  23081  pmatcollpw3fi1lem1  23084  pmatcollpw3fi1lem2  23085  pm2mp  23123  chfacfisf  23152  chfacfisfcpmat  23153  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  chfacfpmmulgsum2  23163  cayhamlem1  23164  cpmadugsumlemF  23174  cpmadugsumfi  23175  cayhamlem2  23182  chcoeffeqlem  23183  cayleyhamilton1  23190  pnrmopn  23641  xkoptsub  23953  xkopt  23954  tmdgsum  24394  imasdsf1olem  24672  rrxnm  25692  rrxds  25694  rrxf  25702  rrxmvallem  25705  rrxbasefi  25711  rrxdsfi  25712  ehlbase  25716  ovolscalem2  25815  uniioombl  25890  tdeglem2  26359  plypf1  26511  ulmclm  26696  ulmcaulem  26703  ulmcau  26704  ulmss  26706  ulmbdd  26707  ulmcn  26708  ulmdvlem1  26709  ulmdvlem2  26710  ulmdvlem3  26711  mtest  26713  mtestbdd  26714  mbfulm  26715  iblulm  26716  itgulm  26717  itgulm2  26718  adjval2  32475  fmptco1f1o  33209  fcobijfs  33295  fcobijfs2  33296  resf1o  33304  fpwrelmap  33307  elrspunidl  33960  elrspunsn  33961  1arithidomlem2  34050  1arithidom  34051  fply1  34072  psrbasfsupp  34125  selvply1rhmlemb  34133  ply1degltdimlem  34236  fedgmullem1  34243  fedgmul  34245  extdg1id  34280  smatrcl  34410  mbfmf  34869  elmbfmvol2  34882  eulerpartlemelr  34972  eulerpartlemf  34985  eulerpartlemt  34986  eulerpartgbij  34987  eulerpartlemgu  34992  eulerpartlemgh  34993  eulerpartlemgf  34994  eulerpartlemgs2  34995  reprf  35224  reprsuc  35227  vtsprod  35251  circlemethhgt  35255  tgoldbachgtd  35274  satfv1lem  36096  satfvel  36146  satefvfmla0  36152  satefvfmla1  36159  prv1n  36165  mrsubff1  36248  mrsub0  36250  mrsubf  36251  mrsubccat  36252  mrsubcn  36253  msubrn  36263  msubff  36264  msubf  36266  msubff1  36290  mclsind  36304  curunc  38493  unccur  38494  poimirlem4  38510  poimirlem5  38511  poimirlem6  38512  poimirlem7  38513  poimirlem8  38514  poimirlem10  38516  poimirlem11  38517  poimirlem12  38518  poimirlem16  38522  poimirlem17  38523  poimirlem18  38524  poimirlem19  38525  poimirlem20  38526  poimirlem21  38527  poimirlem22  38528  poimirlem25  38531  poimirlem26  38532  poimirlem27  38533  poimirlem29  38535  poimirlem30  38536  poimirlem31  38537  poimirlem32  38538  poimir  38539  broucube  38540  mblfinlem3  38545  mblfinlem4  38546  ismblfin  38547  rrnmet  38731  rrndstprj1  38732  rrndstprj2  38733  rrncmslem  38734  rrnequiv  38737  aks6d1c2lem4  43145  mapcod  43262  evlselv  43579  fsuppind  43580  mhphf  43587  mapco2g  43678  mapfzcons1  43681  mapfzcons2  43683  mzpcompact2lem  43715  eldiophb  43721  elmapresaunres2  43735  eq0rabdioph  43740  rexrabdioph  43754  eldioph4b  43771  diophren  43773  rmydioph  43974  rmxdioph  43976  expdiophlem2  43982  expdioph  43983  pw2f1o2val2  44000  wepwsolem  44002  pwfi2f1o  44056  ofoafo  44316  ofoaid1  44318  ofoaid2  44319  ofoaass  44320  ofoacom  44321  rfovcnvf1od  44963  rfovcnvfvd  44966  fsovrfovd  44968  fsovcnvlem  44972  ntrk0kbimka  44998  neik0pk1imk0  45006  ntrclsfveq1  45019  ntrclsfveq2  45020  ntrclsfveq  45021  ntrclsss  45022  ntrclsiso  45026  ntrclsk2  45027  ntrclskb  45028  ntrclsk3  45029  ntrclsk13  45030  ntrclsk4  45031  ntrneifv3  45041  ntrneineine0lem  45042  ntrneineine1lem  45043  ntrneifv4  45044  ntrneiel2  45045  ntrneicls00  45048  ntrneicls11  45049  ntrneiiso  45050  ntrneik2  45051  ntrneikb  45053  ntrneixb  45054  ntrneik3  45055  ntrneix3  45056  ntrneik13  45057  ntrneix13  45058  ntrneik4w  45059  ntrneik4  45060  clsneifv3  45069  clsneifv4  45070  neicvgfv  45080  k0004ss2  45111  k0004val0  45113  mnringbasefd  45175  mnugrud  45227  mapss2  46162  difmap  46163  inmap  46165  difmapsn  46168  ssmapsn  46172  mccllem  46553  dvnprodlem1  46900  dvnprodlem2  46901  fourierdlem11  47072  fourierdlem12  47073  fourierdlem13  47074  fourierdlem14  47075  fourierdlem34  47095  fourierdlem41  47102  fourierdlem48  47108  fourierdlem49  47109  fourierdlem54  47114  fourierdlem63  47123  fourierdlem64  47124  fourierdlem65  47125  fourierdlem69  47129  fourierdlem72  47132  fourierdlem74  47134  fourierdlem75  47135  fourierdlem79  47139  fourierdlem85  47145  fourierdlem88  47148  fourierdlem89  47149  fourierdlem90  47150  fourierdlem91  47151  fourierdlem92  47152  fourierdlem94  47154  fourierdlem97  47157  fourierdlem103  47163  fourierdlem104  47164  fourierdlem111  47171  fourierdlem113  47173  etransclem24  47212  etransclem26  47214  etransclem27  47215  etransclem28  47216  etransclem31  47219  etransclem32  47220  etransclem33  47221  etransclem34  47222  etransclem35  47223  etransclem37  47225  etransclem38  47226  rrxtopnfi  47241  rrndistlt  47244  qndenserrnbllem  47248  rrxsnicc  47254  ioorrnopnlem  47258  subsaliuncl  47312  hoicvr  47502  ovnprodcl  47508  ovnsupge0  47511  ovnlecvr  47512  ovncvrrp  47518  ovn0lem  47519  ovnsubaddlem1  47524  sge0hsphoire  47543  hoidmv1le  47548  hoidmvlelem1  47549  hoidmvlelem2  47550  hoidmvlelem3  47551  hoidmvlelem4  47552  hoidmvlelem5  47553  hoidmvle  47554  ovnhoilem2  47556  ovnlecvr2  47564  ovncvr2  47565  hoiqssbllem1  47576  hoiqssbllem2  47577  hoiqssbllem3  47578  hspmbllem2  47581  opnvonmbllem2  47587  ovolval2lem  47597  ovolval2  47598  ovolval3  47601  ovolval4lem2  47604  ovolval5lem3  47608  ovnovollem1  47610  ovnovollem2  47611  vonvolmbllem  47614  vonvolmbl2  47617  vonvol2  47618  snvonmbl  47640  vonsn  47645  tmachlem-agreeprod  47891  tmachlem-tpopen  47895  iccpartxr  48445  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  intop  49244  assintop  49250  isassintop  49251  ofaddmndmap  49399  rmsupp0  49424  domnmsuppn0  49425  rmsuppss  49426  scmsuppss  49427  gsumlsscl  49436  lincfsuppcl  49469  linccl  49470  lcosn0  49476  lincdifsn  49480  lincsum  49485  lincscm  49486  lincscmcl  49488  islinindfis  49505  lincext1  49510  lincext2  49511  lincext3  49512  lindslinindimp2lem1  49514  lindslinindimp2lem2  49515  lindslinindimp2lem4  49517  lindslinindsimp2lem5  49518  snlindsntor  49527  lincresunitlem2  49532  lincresunit3lem1  49535  lincresunit3lem2  49536  lincresunit3  49537  lincreslvec3  49538  isldepslvec2  49541  zlmodzxzldeplem2  49557  zlmodzxzldeplem3  49558  ldepsnlinclem1  49561  ldepsnlinclem2  49562  1arymaptf1  49698  1arymaptfo  49699  2arympt  49705  2arymaptf1  49709  2arymaptfo  49710  prelrrx2b  49770  eenglngeehlnmlem1  49793  eenglngeehlnmlem2  49794  aacllem  50883  rr3fvcl  50890  crosspdotsumlem  50908  crossp3d  50911