Theorem elmapi 8847

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  Vcvv 3455  ⟶wf 6534  (class class class)co 7412   ↑_m cmap 8825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7987  df-2nd 7988  df-map 8827

This theorem is referenced by:  mapfset  8848  elmapfn  8863  elmapfun  8864  elmapssres  8865  mapsspm  8875  mapfvd  8878  elmapresaun  8879  map0b  8882  mapss  8888  mapsncnv  8892  ralxpmap  8895  mapen  9130  mapxpen  9132  mapunen  9135  mapfienlem1  9366  mapfienlem2  9367  mapfienlem3  9368  mapfien  9369  wemaplem2  9510  wemappo  9512  wemapsolem  9513  wemapso  9514  wemapso2lem  9515  wemapwe  9667  iunmapdisj  10008  fseqenlem1  10009  fseqenlem2  10010  numacn  10034  finacn  10035  acndom  10036  acndom2  10039  infpwfien  10047  infmap2  10201  fin23lem40  10336  isf32lem12  10349  isf34lem6  10365  acncc  10425  pwfseqlem3  10646  pwxpndom2  10651  ramval  17069  ramub  17074  ramcl  17090  prmgaplem7  17118  prmgaplem8  17119  imasdsval2  17571  funcf2  17926  funcpropd  17960  funcestrcsetclem8  18204  funcestrcsetclem9  18205  funcsetcestrclem8  18219  funcsetcestrclem9  18220  mndpsuppss  18824  mndvcl  18856  mndvass  18857  mndvlid  18858  mndvrid  18859  mhmvlin  18860  fsfnn0gsumfsffz  20054  gsummptnn0fzfv  20058  frlmfibas  21893  frlmbas3  21907  frlmipval  21910  frlmphllem  21911  frlmphl  21912  elfilspd  21934  islindf4  21969  psrbagf  22049  mplbas2  22174  ltbwe  22176  evlsvvvallem  22223  evlsvvval  22225  psr1baslem  22326  psr1basf  22342  fvcoe1  22348  coe1mul2lem1  22409  ply1coe  22439  mamures  22535  grpvlinv  22536  grpvrinv  22537  mamucl  22539  mamuass  22540  mamudi  22541  mamudir  22542  mamuvs1  22543  mamuvs2  22544  mamulid  22579  mamurid  22580  mattposcl  22591  mattpostpos  22592  tposmap  22595  mamutpos  22596  matgsumcl  22598  mavmulcl  22685  mavmulass  22687  mavmulsolcl  22689  marepvcl  22707  1marepvmarrepid  22713  mdetleib2  22726  mdetf  22733  mdetdiaglem  22736  mdetrlin  22740  mdetrsca  22741  mdetralt  22746  mdetunilem7  22756  mdetunilem9  22758  maducoeval2  22778  madutpos  22780  madugsum  22781  madurid  22782  cramerimplem1  22821  m2pmfzmap  22885  decpmatval  22903  pmatcollpw3lem  22921  pmatcollpw3fi1lem1  22924  pmatcollpw3fi1lem2  22925  pm2mp  22963  chfacfisf  22992  chfacfisfcpmat  22993  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  chfacfpmmulgsum2  23003  cayhamlem1  23004  cpmadugsumlemF  23014  cpmadugsumfi  23015  cayhamlem2  23022  chcoeffeqlem  23023  cayleyhamilton1  23030  pnrmopn  23481  xkoptsub  23792  xkopt  23793  tmdgsum  24233  imasdsf1olem  24511  rrxnm  25531  rrxds  25533  rrxf  25541  rrxmvallem  25544  rrxbasefi  25550  rrxdsfi  25551  ehlbase  25555  ovolscalem2  25654  uniioombl  25729  tdeglem2  26199  plypf1  26350  ulmclm  26528  ulmcaulem  26535  ulmcau  26536  ulmss  26538  ulmbdd  26539  ulmcn  26540  ulmdvlem1  26541  ulmdvlem2  26542  ulmdvlem3  26543  mtest  26545  mtestbdd  26546  mbfulm  26547  iblulm  26548  itgulm  26549  itgulm2  26550  adjval2  32221  fmptco1f1o  32956  fcobijfs  33044  fcobijfs2  33045  resf1o  33053  fpwrelmap  33056  elrspunidl  33714  elrspunsn  33715  1arithidomlem2  33804  1arithidom  33805  fply1  33826  psrbasfsupp  33879  selvply1rhmlemb  33887  ply1degltdimlem  33990  fedgmullem1  33997  fedgmul  33999  extdg1id  34034  smatrcl  34164  mbfmf  34622  elmbfmvol2  34635  eulerpartlemelr  34725  eulerpartlemf  34738  eulerpartlemt  34739  eulerpartgbij  34740  eulerpartlemgu  34745  eulerpartlemgh  34746  eulerpartlemgf  34747  eulerpartlemgs2  34748  reprf  34977  reprsuc  34980  vtsprod  35004  circlemethhgt  35008  tgoldbachgtd  35027  satfv1lem  35832  satfvel  35882  satefvfmla0  35888  satefvfmla1  35895  prv1n  35901  mrsubff1  35984  mrsub0  35986  mrsubf  35987  mrsubccat  35988  mrsubcn  35989  msubrn  35999  msubff  36000  msubf  36002  msubff1  36026  mclsind  36040  uncf  38228  curunc  38231  unccur  38232  matunitlindflem1  38245  matunitlindflem2  38246  poimirlem4  38253  poimirlem5  38254  poimirlem6  38255  poimirlem7  38256  poimirlem8  38257  poimirlem10  38259  poimirlem11  38260  poimirlem12  38261  poimirlem16  38265  poimirlem17  38266  poimirlem18  38267  poimirlem19  38268  poimirlem20  38269  poimirlem21  38270  poimirlem22  38271  poimirlem25  38274  poimirlem26  38275  poimirlem27  38276  poimirlem29  38278  poimirlem30  38279  poimirlem31  38280  poimirlem32  38281  poimir  38282  broucube  38283  mblfinlem3  38288  mblfinlem4  38289  ismblfin  38290  rrnmet  38458  rrndstprj1  38459  rrndstprj2  38460  rrncmslem  38461  rrnequiv  38464  aks6d1c2lem4  42872  mapcod  42989  evlselv  43301  fsuppind  43302  mhphf  43309  mapco2g  43425  mapfzcons1  43428  mapfzcons2  43430  mzpcompact2lem  43462  eldiophb  43468  elmapresaunres2  43482  eq0rabdioph  43487  rexrabdioph  43501  eldioph4b  43518  diophren  43520  rmydioph  43721  rmxdioph  43723  expdiophlem2  43729  expdioph  43730  pw2f1o2val2  43747  wepwsolem  43749  pwfi2f1o  43803  ofoafo  44063  ofoaid1  44065  ofoaid2  44066  ofoaass  44067  ofoacom  44068  rfovcnvf1od  44710  rfovcnvfvd  44713  fsovrfovd  44715  fsovcnvlem  44719  ntrk0kbimka  44745  neik0pk1imk0  44753  ntrclsfveq1  44766  ntrclsfveq2  44767  ntrclsfveq  44768  ntrclsss  44769  ntrclsiso  44773  ntrclsk2  44774  ntrclskb  44775  ntrclsk3  44776  ntrclsk13  44777  ntrclsk4  44778  ntrneifv3  44788  ntrneineine0lem  44789  ntrneineine1lem  44790  ntrneifv4  44791  ntrneiel2  44792  ntrneicls00  44795  ntrneicls11  44796  ntrneiiso  44797  ntrneik2  44798  ntrneikb  44800  ntrneixb  44801  ntrneik3  44802  ntrneix3  44803  ntrneik13  44804  ntrneix13  44805  ntrneik4w  44806  ntrneik4  44807  clsneifv3  44816  clsneifv4  44817  neicvgfv  44827  k0004ss2  44858  k0004val0  44860  mnringbasefd  44922  mnugrud  44974  mapss2  45902  difmap  45903  inmap  45905  difmapsn  45908  ssmapsn  45912  mccllem  46293  dvnprodlem1  46640  dvnprodlem2  46641  fourierdlem11  46812  fourierdlem12  46813  fourierdlem13  46814  fourierdlem14  46815  fourierdlem34  46835  fourierdlem41  46842  fourierdlem48  46848  fourierdlem49  46849  fourierdlem54  46854  fourierdlem63  46863  fourierdlem64  46864  fourierdlem65  46865  fourierdlem69  46869  fourierdlem72  46872  fourierdlem74  46874  fourierdlem75  46875  fourierdlem79  46879  fourierdlem85  46885  fourierdlem88  46888  fourierdlem89  46889  fourierdlem90  46890  fourierdlem91  46891  fourierdlem92  46892  fourierdlem94  46894  fourierdlem97  46897  fourierdlem103  46903  fourierdlem104  46904  fourierdlem111  46911  fourierdlem113  46913  etransclem24  46952  etransclem26  46954  etransclem27  46955  etransclem28  46956  etransclem31  46959  etransclem32  46960  etransclem33  46961  etransclem34  46962  etransclem35  46963  etransclem37  46965  etransclem38  46966  rrxtopnfi  46981  rrndistlt  46984  qndenserrnbllem  46988  rrxsnicc  46994  ioorrnopnlem  46998  subsaliuncl  47052  hoicvr  47242  ovnprodcl  47248  ovnsupge0  47251  ovnlecvr  47252  ovncvrrp  47258  ovn0lem  47259  ovnsubaddlem1  47264  sge0hsphoire  47283  hoidmv1le  47288  hoidmvlelem1  47289  hoidmvlelem2  47290  hoidmvlelem3  47291  hoidmvlelem4  47292  hoidmvlelem5  47293  hoidmvle  47294  ovnhoilem2  47296  ovnlecvr2  47304  ovncvr2  47305  hoiqssbllem1  47316  hoiqssbllem2  47317  hoiqssbllem3  47318  hspmbllem2  47321  opnvonmbllem2  47327  ovolval2lem  47337  ovolval2  47338  ovolval3  47341  ovolval4lem2  47344  ovolval5lem3  47348  ovnovollem1  47350  ovnovollem2  47351  vonvolmbllem  47354  vonvolmbl2  47357  vonvol2  47358  snvonmbl  47380  vonsn  47385  iccpartxr  48145  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  intop  48945  assintop  48951  isassintop  48952  ofaddmndmap  49100  rmsupp0  49125  domnmsuppn0  49126  rmsuppss  49127  scmsuppss  49128  gsumlsscl  49137  lincfsuppcl  49170  linccl  49171  lcosn0  49177  lincdifsn  49181  lincsum  49186  lincscm  49187  lincscmcl  49189  islinindfis  49206  lincext1  49211  lincext2  49212  lincext3  49213  lindslinindimp2lem1  49215  lindslinindimp2lem2  49216  lindslinindimp2lem4  49218  lindslinindsimp2lem5  49219  snlindsntor  49228  lincresunitlem2  49233  lincresunit3lem1  49236  lincresunit3lem2  49237  lincresunit3  49238  lincreslvec3  49239  isldepslvec2  49242  zlmodzxzldeplem2  49258  zlmodzxzldeplem3  49259  ldepsnlinclem1  49262  ldepsnlinclem2  49263  1arymaptf1  49399  1arymaptfo  49400  2arympt  49406  2arymaptf1  49410  2arymaptfo  49411  prelrrx2b  49471  eenglngeehlnmlem1  49494  eenglngeehlnmlem2  49495  aacllem  50578