Theorem elmapi 8855

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 8854	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8845	. . 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 2146  Vcvv 3458  ⟶wf 6539  (class class class)co 7423   ↑_m cmap 8833

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-1st 7995  df-2nd 7996  df-map 8835

This theorem is used by:  mapfset  8856  elmapfn  8871  elmapfun  8872  elmapssres  8873  mapsspm  8883  mapfvd  8886  elmapresaun  8887  map0b  8890  mapss  8896  mapsncnv  8900  ralxpmap  8903  mapen  9139  mapxpen  9141  mapunen  9144  mapfienlem1  9375  mapfienlem2  9376  mapfienlem3  9377  mapfien  9378  wemaplem2  9519  wemappo  9521  wemapsolem  9522  wemapso  9523  wemapso2lem  9524  wemapwe  9676  iunmapdisj  10026  fseqenlem1  10027  fseqenlem2  10028  numacn  10052  finacn  10053  acndom  10054  acndom2  10057  infpwfien  10065  infmap2  10219  fin23lem40  10353  isf32lem12  10366  isf34lem6  10382  acncc  10442  pwfseqlem3  10663  pwxpndom2  10668  ramval  17093  ramub  17098  ramcl  17114  prmgaplem7  17142  prmgaplem8  17143  imasdsval2  17595  funcf2  17950  funcpropd  17984  funcestrcsetclem8  18228  funcestrcsetclem9  18229  funcsetcestrclem8  18243  funcsetcestrclem9  18244  mndpsuppss  18854  mndvcl  18886  mndvass  18887  mndvlid  18888  mndvrid  18889  mhmvlin  18890  fsfnn0gsumfsffz  20084  gsummptnn0fzfv  20088  frlmfibas  21949  frlmbas3  21963  frlmipval  21966  frlmphllem  21967  frlmphl  21968  elfilspd  21990  islindf4  22025  psrbagf  22105  mplbas2  22230  ltbwe  22232  evlsvvvallem  22279  evlsvvval  22281  psr1baslem  22382  psr1basf  22398  fvcoe1  22404  coe1mul2lem1  22465  ply1coe  22495  mamures  22591  grpvlinv  22592  grpvrinv  22593  mamucl  22595  mamuass  22596  mamudi  22597  mamudir  22598  mamuvs1  22599  mamuvs2  22600  mamulid  22635  mamurid  22636  mattposcl  22647  mattpostpos  22648  tposmap  22651  mamutpos  22652  matgsumcl  22654  mavmulcl  22741  mavmulass  22743  mavmulsolcl  22745  marepvcl  22763  1marepvmarrepid  22769  mdetleib2  22782  mdetf  22789  mdetdiaglem  22792  mdetrlin  22796  mdetrsca  22797  mdetralt  22802  mdetunilem7  22812  mdetunilem9  22814  maducoeval2  22834  madutpos  22836  madugsum  22837  madurid  22838  cramerimplem1  22877  m2pmfzmap  22941  decpmatval  22959  pmatcollpw3lem  22977  pmatcollpw3fi1lem1  22980  pmatcollpw3fi1lem2  22981  pm2mp  23019  chfacfisf  23048  chfacfisfcpmat  23049  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  chfacfpmmulgsum2  23059  cayhamlem1  23060  cpmadugsumlemF  23070  cpmadugsumfi  23071  cayhamlem2  23078  chcoeffeqlem  23079  cayleyhamilton1  23086  pnrmopn  23537  xkoptsub  23848  xkopt  23849  tmdgsum  24289  imasdsf1olem  24567  rrxnm  25587  rrxds  25589  rrxf  25597  rrxmvallem  25600  rrxbasefi  25606  rrxdsfi  25607  ehlbase  25611  ovolscalem2  25710  uniioombl  25785  tdeglem2  26255  plypf1  26406  ulmclm  26587  ulmcaulem  26594  ulmcau  26595  ulmss  26597  ulmbdd  26598  ulmcn  26599  ulmdvlem1  26600  ulmdvlem2  26601  ulmdvlem3  26602  mtest  26604  mtestbdd  26605  mbfulm  26606  iblulm  26607  itgulm  26608  itgulm2  26609  adjval2  32280  fmptco1f1o  33015  fcobijfs  33103  fcobijfs2  33104  resf1o  33112  fpwrelmap  33115  elrspunidl  33767  elrspunsn  33768  1arithidomlem2  33857  1arithidom  33858  fply1  33879  psrbasfsupp  33932  selvply1rhmlemb  33940  ply1degltdimlem  34043  fedgmullem1  34050  fedgmul  34052  extdg1id  34087  smatrcl  34217  mbfmf  34675  elmbfmvol2  34688  eulerpartlemelr  34778  eulerpartlemf  34791  eulerpartlemt  34792  eulerpartgbij  34793  eulerpartlemgu  34798  eulerpartlemgh  34799  eulerpartlemgf  34800  eulerpartlemgs2  34801  reprf  35030  reprsuc  35033  vtsprod  35057  circlemethhgt  35061  tgoldbachgtd  35080  satfv1lem  35874  satfvel  35924  satefvfmla0  35930  satefvfmla1  35937  prv1n  35943  mrsubff1  36026  mrsub0  36028  mrsubf  36029  mrsubccat  36030  mrsubcn  36031  msubrn  36041  msubff  36042  msubf  36044  msubff1  36068  mclsind  36082  uncf  38290  curunc  38293  unccur  38294  matunitlindflem1  38307  matunitlindflem2  38308  poimirlem4  38315  poimirlem5  38316  poimirlem6  38317  poimirlem7  38318  poimirlem8  38319  poimirlem10  38321  poimirlem11  38322  poimirlem12  38323  poimirlem16  38327  poimirlem17  38328  poimirlem18  38329  poimirlem19  38330  poimirlem20  38331  poimirlem21  38332  poimirlem22  38333  poimirlem25  38336  poimirlem26  38337  poimirlem27  38338  poimirlem29  38340  poimirlem30  38341  poimirlem31  38342  poimirlem32  38343  poimir  38344  broucube  38345  mblfinlem3  38350  mblfinlem4  38351  ismblfin  38352  rrnmet  38520  rrndstprj1  38521  rrndstprj2  38522  rrncmslem  38523  rrnequiv  38526  aks6d1c2lem4  42934  mapcod  43051  evlselv  43361  fsuppind  43362  mhphf  43369  mapco2g  43485  mapfzcons1  43488  mapfzcons2  43490  mzpcompact2lem  43522  eldiophb  43528  elmapresaunres2  43542  eq0rabdioph  43547  rexrabdioph  43561  eldioph4b  43578  diophren  43580  rmydioph  43781  rmxdioph  43783  expdiophlem2  43789  expdioph  43790  pw2f1o2val2  43807  wepwsolem  43809  pwfi2f1o  43863  ofoafo  44123  ofoaid1  44125  ofoaid2  44126  ofoaass  44127  ofoacom  44128  rfovcnvf1od  44770  rfovcnvfvd  44773  fsovrfovd  44775  fsovcnvlem  44779  ntrk0kbimka  44805  neik0pk1imk0  44813  ntrclsfveq1  44826  ntrclsfveq2  44827  ntrclsfveq  44828  ntrclsss  44829  ntrclsiso  44833  ntrclsk2  44834  ntrclskb  44835  ntrclsk3  44836  ntrclsk13  44837  ntrclsk4  44838  ntrneifv3  44848  ntrneineine0lem  44849  ntrneineine1lem  44850  ntrneifv4  44851  ntrneiel2  44852  ntrneicls00  44855  ntrneicls11  44856  ntrneiiso  44857  ntrneik2  44858  ntrneikb  44860  ntrneixb  44861  ntrneik3  44862  ntrneix3  44863  ntrneik13  44864  ntrneix13  44865  ntrneik4w  44866  ntrneik4  44867  clsneifv3  44876  clsneifv4  44877  neicvgfv  44887  k0004ss2  44918  k0004val0  44920  mnringbasefd  44982  mnugrud  45034  mapss2  45962  difmap  45963  inmap  45965  difmapsn  45968  ssmapsn  45972  mccllem  46353  dvnprodlem1  46700  dvnprodlem2  46701  fourierdlem11  46872  fourierdlem12  46873  fourierdlem13  46874  fourierdlem14  46875  fourierdlem34  46895  fourierdlem41  46902  fourierdlem48  46908  fourierdlem49  46909  fourierdlem54  46914  fourierdlem63  46923  fourierdlem64  46924  fourierdlem65  46925  fourierdlem69  46929  fourierdlem72  46932  fourierdlem74  46934  fourierdlem75  46935  fourierdlem79  46939  fourierdlem85  46945  fourierdlem88  46948  fourierdlem89  46949  fourierdlem90  46950  fourierdlem91  46951  fourierdlem92  46952  fourierdlem94  46954  fourierdlem97  46957  fourierdlem103  46963  fourierdlem104  46964  fourierdlem111  46971  fourierdlem113  46973  etransclem24  47012  etransclem26  47014  etransclem27  47015  etransclem28  47016  etransclem31  47019  etransclem32  47020  etransclem33  47021  etransclem34  47022  etransclem35  47023  etransclem37  47025  etransclem38  47026  rrxtopnfi  47041  rrndistlt  47044  qndenserrnbllem  47048  rrxsnicc  47054  ioorrnopnlem  47058  subsaliuncl  47112  hoicvr  47302  ovnprodcl  47308  ovnsupge0  47311  ovnlecvr  47312  ovncvrrp  47318  ovn0lem  47319  ovnsubaddlem1  47324  sge0hsphoire  47343  hoidmv1le  47348  hoidmvlelem1  47349  hoidmvlelem2  47350  hoidmvlelem3  47351  hoidmvlelem4  47352  hoidmvlelem5  47353  hoidmvle  47354  ovnhoilem2  47356  ovnlecvr2  47364  ovncvr2  47365  hoiqssbllem1  47376  hoiqssbllem2  47377  hoiqssbllem3  47378  hspmbllem2  47381  opnvonmbllem2  47387  ovolval2lem  47397  ovolval2  47398  ovolval3  47401  ovolval4lem2  47404  ovolval5lem3  47408  ovnovollem1  47410  ovnovollem2  47411  vonvolmbllem  47414  vonvolmbl2  47417  vonvol2  47418  snvonmbl  47440  vonsn  47445  iccpartxr  48208  nnsum4primeseven  48605  nnsum4primesevenALTV  48606  intop  49008  assintop  49014  isassintop  49015  ofaddmndmap  49163  rmsupp0  49188  domnmsuppn0  49189  rmsuppss  49190  scmsuppss  49191  gsumlsscl  49200  lincfsuppcl  49233  linccl  49234  lcosn0  49240  lincdifsn  49244  lincsum  49249  lincscm  49250  lincscmcl  49252  islinindfis  49269  lincext1  49274  lincext2  49275  lincext3  49276  lindslinindimp2lem1  49278  lindslinindimp2lem2  49279  lindslinindimp2lem4  49281  lindslinindsimp2lem5  49282  snlindsntor  49291  lincresunitlem2  49296  lincresunit3lem1  49299  lincresunit3lem2  49300  lincresunit3  49301  lincreslvec3  49302  isldepslvec2  49305  zlmodzxzldeplem2  49321  zlmodzxzldeplem3  49322  ldepsnlinclem1  49325  ldepsnlinclem2  49326  1arymaptf1  49462  1arymaptfo  49463  2arympt  49469  2arymaptf1  49473  2arymaptfo  49474  prelrrx2b  49534  eenglngeehlnmlem1  49557  eenglngeehlnmlem2  49558  aacllem  50661  rr3fvcl  50668  crosspdotsumi  50686  crossp3i  50689