Theorem elmapi 8861

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 8860	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8851	. . 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 3459  ⟶wf 6526  (class class class)co 7403   ↑_m cmap 8838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-fv 6538  df-ov 7406  df-oprab 7407  df-mpo 7408  df-1st 7986  df-2nd 7987  df-map 8840

This theorem is referenced by:  mapfset  8862  elmapfn  8877  elmapfun  8878  elmapssres  8879  mapsspm  8888  mapfvd  8891  elmapresaun  8892  map0b  8895  mapss  8901  mapsncnv  8905  ralxpmap  8908  mapen  9153  mapxpen  9155  mapunen  9158  mapfienlem1  9415  mapfienlem2  9416  mapfienlem3  9417  mapfien  9418  wemaplem2  9559  wemappo  9561  wemapsolem  9562  wemapso  9563  wemapso2lem  9564  wemapwe  9709  iunmapdisj  10035  fseqenlem1  10036  fseqenlem2  10037  numacn  10061  finacn  10062  acndom  10063  acndom2  10066  infpwfien  10074  infmap2  10229  fin23lem40  10363  isf32lem12  10376  isf34lem6  10392  acncc  10452  pwfseqlem3  10672  pwxpndom2  10677  ramval  17026  ramub  17031  ramcl  17047  prmgaplem7  17075  prmgaplem8  17076  imasdsval2  17528  funcf2  17879  funcpropd  17913  funcestrcsetclem8  18157  funcestrcsetclem9  18158  funcsetcestrclem8  18172  funcsetcestrclem9  18173  mndpsuppss  18741  mndvcl  18773  mndvass  18774  mndvlid  18775  mndvrid  18776  mhmvlin  18777  fsfnn0gsumfsffz  19962  gsummptnn0fzfv  19966  frlmfibas  21720  frlmbas3  21734  frlmipval  21737  frlmphllem  21738  frlmphl  21739  elfilspd  21761  islindf4  21796  psrbagf  21876  mplbas2  21998  ltbwe  22000  psr1baslem  22118  psr1basf  22135  fvcoe1  22141  coe1mul2lem1  22202  ply1coe  22234  mamures  22333  grpvlinv  22334  grpvrinv  22335  mamucl  22337  mamuass  22338  mamudi  22339  mamudir  22340  mamuvs1  22341  mamuvs2  22342  mamulid  22377  mamurid  22378  mattposcl  22389  mattpostpos  22390  tposmap  22393  mamutpos  22394  matgsumcl  22396  mavmulcl  22483  mavmulass  22485  mavmulsolcl  22487  marepvcl  22505  1marepvmarrepid  22511  mdetleib2  22524  mdetf  22531  mdetdiaglem  22534  mdetrlin  22538  mdetrsca  22539  mdetralt  22544  mdetunilem7  22554  mdetunilem9  22556  maducoeval2  22576  madutpos  22578  madugsum  22579  madurid  22580  cramerimplem1  22619  m2pmfzmap  22683  decpmatval  22701  pmatcollpw3lem  22719  pmatcollpw3fi1lem1  22722  pmatcollpw3fi1lem2  22723  pm2mp  22761  chfacfisf  22790  chfacfisfcpmat  22791  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  chfacfpmmulgsum2  22801  cayhamlem1  22802  cpmadugsumlemF  22812  cpmadugsumfi  22813  cayhamlem2  22820  chcoeffeqlem  22821  cayleyhamilton1  22828  pnrmopn  23279  xkoptsub  23590  xkopt  23591  tmdgsum  24031  imasdsf1olem  24310  rrxnm  25341  rrxds  25343  rrxf  25351  rrxmvallem  25354  rrxbasefi  25360  rrxdsfi  25361  ehlbase  25365  ovolscalem2  25465  uniioombl  25540  tdeglem2  26016  plypf1  26167  ulmclm  26346  ulmcaulem  26353  ulmcau  26354  ulmss  26356  ulmbdd  26357  ulmcn  26358  ulmdvlem1  26359  ulmdvlem2  26360  ulmdvlem3  26361  mtest  26363  mtestbdd  26364  mbfulm  26365  iblulm  26366  itgulm  26367  itgulm2  26368  adjval2  31818  fmptco1f1o  32557  fcobijfs  32646  resf1o  32653  fpwrelmap  32656  elrspunidl  33389  elrspunsn  33390  1arithidomlem2  33497  1arithidom  33498  fply1  33517  ply1degltdimlem  33608  fedgmullem1  33615  fedgmul  33617  extdg1id  33653  smatrcl  33773  mbfmf  34231  elmbfmvol2  34245  eulerpartlemelr  34335  eulerpartlemf  34348  eulerpartlemt  34349  eulerpartgbij  34350  eulerpartlemgu  34355  eulerpartlemgh  34356  eulerpartlemgf  34357  eulerpartlemgs2  34358  reprf  34590  reprsuc  34593  vtsprod  34617  circlemethhgt  34621  tgoldbachgtd  34640  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  37569  curunc  37572  unccur  37573  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem4  37594  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  poimir  37623  broucube  37624  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  rrnmet  37799  rrndstprj1  37800  rrndstprj2  37801  rrncmslem  37802  rrnequiv  37805  aks6d1c2lem4  42086  mapcod  42241  evlsvvvallem  42531  evlsvvval  42533  evlselv  42557  fsuppind  42560  mhphf  42567  mapco2g  42684  mapfzcons1  42687  mapfzcons2  42689  mzpcompact2lem  42721  eldiophb  42727  elmapresaunres2  42741  eq0rabdioph  42746  rexrabdioph  42764  eldioph4b  42781  diophren  42783  rmydioph  42985  rmxdioph  42987  expdiophlem2  42993  expdioph  42994  pw2f1o2val2  43011  wepwsolem  43013  pwfi2f1o  43067  ofoafo  43327  ofoaid1  43329  ofoaid2  43330  ofoaass  43331  ofoacom  43332  rfovcnvf1od  43975  rfovcnvfvd  43978  fsovrfovd  43980  fsovcnvlem  43984  ntrk0kbimka  44010  neik0pk1imk0  44018  ntrclsfveq1  44031  ntrclsfveq2  44032  ntrclsfveq  44033  ntrclsss  44034  ntrclsiso  44038  ntrclsk2  44039  ntrclskb  44040  ntrclsk3  44041  ntrclsk13  44042  ntrclsk4  44043  ntrneifv3  44053  ntrneineine0lem  44054  ntrneineine1lem  44055  ntrneifv4  44056  ntrneiel2  44057  ntrneicls00  44060  ntrneicls11  44061  ntrneiiso  44062  ntrneik2  44063  ntrneikb  44065  ntrneixb  44066  ntrneik3  44067  ntrneix3  44068  ntrneik13  44069  ntrneix13  44070  ntrneik4w  44071  ntrneik4  44072  clsneifv3  44081  clsneifv4  44082  neicvgfv  44092  k0004ss2  44123  k0004val0  44125  mnringbasefd  44190  mnugrud  44256  mapss2  45177  difmap  45179  inmap  45181  difmapsn  45184  ssmapsn  45188  mccllem  45574  dvnprodlem1  45923  dvnprodlem2  45924  fourierdlem11  46095  fourierdlem12  46096  fourierdlem13  46097  fourierdlem14  46098  fourierdlem34  46118  fourierdlem41  46125  fourierdlem48  46131  fourierdlem49  46132  fourierdlem54  46137  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem69  46152  fourierdlem72  46155  fourierdlem74  46157  fourierdlem75  46158  fourierdlem79  46162  fourierdlem85  46168  fourierdlem88  46171  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem92  46175  fourierdlem94  46177  fourierdlem97  46180  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem113  46196  etransclem24  46235  etransclem26  46237  etransclem27  46238  etransclem28  46239  etransclem31  46242  etransclem32  46243  etransclem33  46244  etransclem34  46245  etransclem35  46246  etransclem37  46248  etransclem38  46249  rrxtopnfi  46264  rrndistlt  46267  qndenserrnbllem  46271  rrxsnicc  46277  ioorrnopnlem  46281  subsaliuncl  46335  hoicvr  46525  ovnprodcl  46531  ovnsupge0  46534  ovnlecvr  46535  ovncvrrp  46541  ovn0lem  46542  ovnsubaddlem1  46547  sge0hsphoire  46566  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  hoidmvlelem5  46576  hoidmvle  46577  ovnhoilem2  46579  ovnlecvr2  46587  ovncvr2  46588  hoiqssbllem1  46599  hoiqssbllem2  46600  hoiqssbllem3  46601  hspmbllem2  46604  opnvonmbllem2  46610  ovolval2lem  46620  ovolval2  46621  ovolval3  46624  ovolval4lem2  46627  ovolval5lem3  46631  ovnovollem1  46633  ovnovollem2  46634  vonvolmbllem  46637  vonvolmbl2  46640  vonvol2  46641  snvonmbl  46663  vonsn  46668  iccpartxr  47381  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  intop  48126  assintop  48132  isassintop  48133  ofaddmndmap  48266  rmsupp0  48291  domnmsuppn0  48292  rmsuppss  48293  scmsuppss  48294  gsumlsscl  48303  lincfsuppcl  48337  linccl  48338  lcosn0  48344  lincdifsn  48348  lincsum  48353  lincscm  48354  lincscmcl  48356  islinindfis  48373  lincext1  48378  lincext2  48379  lincext3  48380  lindslinindimp2lem1  48382  lindslinindimp2lem2  48383  lindslinindimp2lem4  48385  lindslinindsimp2lem5  48386  snlindsntor  48395  lincresunitlem2  48400  lincresunit3lem1  48403  lincresunit3lem2  48404  lincresunit3  48405  lincreslvec3  48406  isldepslvec2  48409  zlmodzxzldeplem2  48425  zlmodzxzldeplem3  48426  ldepsnlinclem1  48429  ldepsnlinclem2  48430  1arymaptf1  48570  1arymaptfo  48571  2arympt  48577  2arymaptf1  48581  2arymaptfo  48582  prelrrx2b  48642  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  aacllem  49613