Theorem elmapi 8786

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 8785	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8776	. . 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 2113  Vcvv 3440  ⟶wf 6488  (class class class)co 7358   ↑_m cmap 8763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-map 8765

This theorem is referenced by:  mapfset  8787  elmapfn  8802  elmapfun  8803  elmapssres  8804  mapsspm  8814  mapfvd  8817  elmapresaun  8818  map0b  8821  mapss  8827  mapsncnv  8831  ralxpmap  8834  mapen  9069  mapxpen  9071  mapunen  9074  mapfienlem1  9308  mapfienlem2  9309  mapfienlem3  9310  mapfien  9311  wemaplem2  9452  wemappo  9454  wemapsolem  9455  wemapso  9456  wemapso2lem  9457  wemapwe  9606  iunmapdisj  9933  fseqenlem1  9934  fseqenlem2  9935  numacn  9959  finacn  9960  acndom  9961  acndom2  9964  infpwfien  9972  infmap2  10127  fin23lem40  10261  isf32lem12  10274  isf34lem6  10290  acncc  10350  pwfseqlem3  10571  pwxpndom2  10576  ramval  16936  ramub  16941  ramcl  16957  prmgaplem7  16985  prmgaplem8  16986  imasdsval2  17437  funcf2  17792  funcpropd  17826  funcestrcsetclem8  18070  funcestrcsetclem9  18071  funcsetcestrclem8  18085  funcsetcestrclem9  18086  mndpsuppss  18690  mndvcl  18722  mndvass  18723  mndvlid  18724  mndvrid  18725  mhmvlin  18726  fsfnn0gsumfsffz  19912  gsummptnn0fzfv  19916  frlmfibas  21717  frlmbas3  21731  frlmipval  21734  frlmphllem  21735  frlmphl  21736  elfilspd  21758  islindf4  21793  psrbagf  21874  mplbas2  21997  ltbwe  21999  evlsvvvallem  22046  evlsvvval  22048  psr1baslem  22125  psr1basf  22142  fvcoe1  22148  coe1mul2lem1  22209  ply1coe  22242  mamures  22341  grpvlinv  22342  grpvrinv  22343  mamucl  22345  mamuass  22346  mamudi  22347  mamudir  22348  mamuvs1  22349  mamuvs2  22350  mamulid  22385  mamurid  22386  mattposcl  22397  mattpostpos  22398  tposmap  22401  mamutpos  22402  matgsumcl  22404  mavmulcl  22491  mavmulass  22493  mavmulsolcl  22495  marepvcl  22513  1marepvmarrepid  22519  mdetleib2  22532  mdetf  22539  mdetdiaglem  22542  mdetrlin  22546  mdetrsca  22547  mdetralt  22552  mdetunilem7  22562  mdetunilem9  22564  maducoeval2  22584  madutpos  22586  madugsum  22587  madurid  22588  cramerimplem1  22627  m2pmfzmap  22691  decpmatval  22709  pmatcollpw3lem  22727  pmatcollpw3fi1lem1  22730  pmatcollpw3fi1lem2  22731  pm2mp  22769  chfacfisf  22798  chfacfisfcpmat  22799  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  chfacfpmmulgsum2  22809  cayhamlem1  22810  cpmadugsumlemF  22820  cpmadugsumfi  22821  cayhamlem2  22828  chcoeffeqlem  22829  cayleyhamilton1  22836  pnrmopn  23287  xkoptsub  23598  xkopt  23599  tmdgsum  24039  imasdsf1olem  24317  rrxnm  25347  rrxds  25349  rrxf  25357  rrxmvallem  25360  rrxbasefi  25366  rrxdsfi  25367  ehlbase  25371  ovolscalem2  25471  uniioombl  25546  tdeglem2  26022  plypf1  26173  ulmclm  26352  ulmcaulem  26359  ulmcau  26360  ulmss  26362  ulmbdd  26363  ulmcn  26364  ulmdvlem1  26365  ulmdvlem2  26366  ulmdvlem3  26367  mtest  26369  mtestbdd  26370  mbfulm  26371  iblulm  26372  itgulm  26373  itgulm2  26374  adjval2  31966  fmptco1f1o  32711  fcobijfs  32800  fcobijfs2  32801  resf1o  32809  fpwrelmap  32812  elrspunidl  33509  elrspunsn  33510  1arithidomlem2  33617  1arithidom  33618  fply1  33639  psrbasfsupp  33693  ply1degltdimlem  33779  fedgmullem1  33786  fedgmul  33788  extdg1id  33823  smatrcl  33953  mbfmf  34411  elmbfmvol2  34424  eulerpartlemelr  34514  eulerpartlemf  34527  eulerpartlemt  34528  eulerpartgbij  34529  eulerpartlemgu  34534  eulerpartlemgh  34535  eulerpartlemgf  34536  eulerpartlemgs2  34537  reprf  34769  reprsuc  34772  vtsprod  34796  circlemethhgt  34800  tgoldbachgtd  34819  satfv1lem  35556  satfvel  35606  satefvfmla0  35612  satefvfmla1  35619  prv1n  35625  mrsubff1  35708  mrsub0  35710  mrsubf  35711  mrsubccat  35712  mrsubcn  35713  msubrn  35723  msubff  35724  msubf  35726  msubff1  35750  mclsind  35764  uncf  37796  curunc  37799  unccur  37800  matunitlindflem1  37813  matunitlindflem2  37814  poimirlem4  37821  poimirlem5  37822  poimirlem6  37823  poimirlem7  37824  poimirlem8  37825  poimirlem10  37827  poimirlem11  37828  poimirlem12  37829  poimirlem16  37833  poimirlem17  37834  poimirlem18  37835  poimirlem19  37836  poimirlem20  37837  poimirlem21  37838  poimirlem22  37839  poimirlem25  37842  poimirlem26  37843  poimirlem27  37844  poimirlem29  37846  poimirlem30  37847  poimirlem31  37848  poimirlem32  37849  poimir  37850  broucube  37851  mblfinlem3  37856  mblfinlem4  37857  ismblfin  37858  rrnmet  38026  rrndstprj1  38027  rrndstprj2  38028  rrncmslem  38029  rrnequiv  38032  aks6d1c2lem4  42377  mapcod  42494  evlselv  42826  fsuppind  42829  mhphf  42836  mapco2g  42952  mapfzcons1  42955  mapfzcons2  42957  mzpcompact2lem  42989  eldiophb  42995  elmapresaunres2  43009  eq0rabdioph  43014  rexrabdioph  43032  eldioph4b  43049  diophren  43051  rmydioph  43252  rmxdioph  43254  expdiophlem2  43260  expdioph  43261  pw2f1o2val2  43278  wepwsolem  43280  pwfi2f1o  43334  ofoafo  43594  ofoaid1  43596  ofoaid2  43597  ofoaass  43598  ofoacom  43599  rfovcnvf1od  44241  rfovcnvfvd  44244  fsovrfovd  44246  fsovcnvlem  44250  ntrk0kbimka  44276  neik0pk1imk0  44284  ntrclsfveq1  44297  ntrclsfveq2  44298  ntrclsfveq  44299  ntrclsss  44300  ntrclsiso  44304  ntrclsk2  44305  ntrclskb  44306  ntrclsk3  44307  ntrclsk13  44308  ntrclsk4  44309  ntrneifv3  44319  ntrneineine0lem  44320  ntrneineine1lem  44321  ntrneifv4  44322  ntrneiel2  44323  ntrneicls00  44326  ntrneicls11  44327  ntrneiiso  44328  ntrneik2  44329  ntrneikb  44331  ntrneixb  44332  ntrneik3  44333  ntrneix3  44334  ntrneik13  44335  ntrneix13  44336  ntrneik4w  44337  ntrneik4  44338  clsneifv3  44347  clsneifv4  44348  neicvgfv  44358  k0004ss2  44389  k0004val0  44391  mnringbasefd  44455  mnugrud  44521  mapss2  45445  difmap  45447  inmap  45449  difmapsn  45452  ssmapsn  45456  mccllem  45839  dvnprodlem1  46186  dvnprodlem2  46187  fourierdlem11  46358  fourierdlem12  46359  fourierdlem13  46360  fourierdlem14  46361  fourierdlem34  46381  fourierdlem41  46388  fourierdlem48  46394  fourierdlem49  46395  fourierdlem54  46400  fourierdlem63  46409  fourierdlem64  46410  fourierdlem65  46411  fourierdlem69  46415  fourierdlem72  46418  fourierdlem74  46420  fourierdlem75  46421  fourierdlem79  46425  fourierdlem85  46431  fourierdlem88  46434  fourierdlem89  46435  fourierdlem90  46436  fourierdlem91  46437  fourierdlem92  46438  fourierdlem94  46440  fourierdlem97  46443  fourierdlem103  46449  fourierdlem104  46450  fourierdlem111  46457  fourierdlem113  46459  etransclem24  46498  etransclem26  46500  etransclem27  46501  etransclem28  46502  etransclem31  46505  etransclem32  46506  etransclem33  46507  etransclem34  46508  etransclem35  46509  etransclem37  46511  etransclem38  46512  rrxtopnfi  46527  rrndistlt  46530  qndenserrnbllem  46534  rrxsnicc  46540  ioorrnopnlem  46544  subsaliuncl  46598  hoicvr  46788  ovnprodcl  46794  ovnsupge0  46797  ovnlecvr  46798  ovncvrrp  46804  ovn0lem  46805  ovnsubaddlem1  46810  sge0hsphoire  46829  hoidmv1le  46834  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem3  46837  hoidmvlelem4  46838  hoidmvlelem5  46839  hoidmvle  46840  ovnhoilem2  46842  ovnlecvr2  46850  ovncvr2  46851  hoiqssbllem1  46862  hoiqssbllem2  46863  hoiqssbllem3  46864  hspmbllem2  46867  opnvonmbllem2  46873  ovolval2lem  46883  ovolval2  46884  ovolval3  46887  ovolval4lem2  46890  ovolval5lem3  46894  ovnovollem1  46896  ovnovollem2  46897  vonvolmbllem  46900  vonvolmbl2  46903  vonvol2  46904  snvonmbl  46926  vonsn  46931  iccpartxr  47661  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  intop  48445  assintop  48451  isassintop  48452  ofaddmndmap  48585  rmsupp0  48610  domnmsuppn0  48611  rmsuppss  48612  scmsuppss  48613  gsumlsscl  48622  lincfsuppcl  48655  linccl  48656  lcosn0  48662  lincdifsn  48666  lincsum  48671  lincscm  48672  lincscmcl  48674  islinindfis  48691  lincext1  48696  lincext2  48697  lincext3  48698  lindslinindimp2lem1  48700  lindslinindimp2lem2  48701  lindslinindimp2lem4  48703  lindslinindsimp2lem5  48704  snlindsntor  48713  lincresunitlem2  48718  lincresunit3lem1  48721  lincresunit3lem2  48722  lincresunit3  48723  lincreslvec3  48724  isldepslvec2  48727  zlmodzxzldeplem2  48743  zlmodzxzldeplem3  48744  ldepsnlinclem1  48747  ldepsnlinclem2  48748  1arymaptf1  48884  1arymaptfo  48885  2arympt  48891  2arymaptf1  48895  2arymaptfo  48896  prelrrx2b  48956  eenglngeehlnmlem1  48979  eenglngeehlnmlem2  48980  aacllem  50042