Theorem elmapi 8798

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 8797	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8788	. . 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 2114  Vcvv 3442  ⟶wf 6496  (class class class)co 7368   ↑_m cmap 8775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-map 8777

This theorem is referenced by:  mapfset  8799  elmapfn  8814  elmapfun  8815  elmapssres  8816  mapsspm  8826  mapfvd  8829  elmapresaun  8830  map0b  8833  mapss  8839  mapsncnv  8843  ralxpmap  8846  mapen  9081  mapxpen  9083  mapunen  9086  mapfienlem1  9320  mapfienlem2  9321  mapfienlem3  9322  mapfien  9323  wemaplem2  9464  wemappo  9466  wemapsolem  9467  wemapso  9468  wemapso2lem  9469  wemapwe  9618  iunmapdisj  9945  fseqenlem1  9946  fseqenlem2  9947  numacn  9971  finacn  9972  acndom  9973  acndom2  9976  infpwfien  9984  infmap2  10139  fin23lem40  10273  isf32lem12  10286  isf34lem6  10302  acncc  10362  pwfseqlem3  10583  pwxpndom2  10588  ramval  16948  ramub  16953  ramcl  16969  prmgaplem7  16997  prmgaplem8  16998  imasdsval2  17449  funcf2  17804  funcpropd  17838  funcestrcsetclem8  18082  funcestrcsetclem9  18083  funcsetcestrclem8  18097  funcsetcestrclem9  18098  mndpsuppss  18702  mndvcl  18734  mndvass  18735  mndvlid  18736  mndvrid  18737  mhmvlin  18738  fsfnn0gsumfsffz  19924  gsummptnn0fzfv  19928  frlmfibas  21729  frlmbas3  21743  frlmipval  21746  frlmphllem  21747  frlmphl  21748  elfilspd  21770  islindf4  21805  psrbagf  21886  mplbas2  22009  ltbwe  22011  evlsvvvallem  22058  evlsvvval  22060  psr1baslem  22137  psr1basf  22154  fvcoe1  22160  coe1mul2lem1  22221  ply1coe  22254  mamures  22353  grpvlinv  22354  grpvrinv  22355  mamucl  22357  mamuass  22358  mamudi  22359  mamudir  22360  mamuvs1  22361  mamuvs2  22362  mamulid  22397  mamurid  22398  mattposcl  22409  mattpostpos  22410  tposmap  22413  mamutpos  22414  matgsumcl  22416  mavmulcl  22503  mavmulass  22505  mavmulsolcl  22507  marepvcl  22525  1marepvmarrepid  22531  mdetleib2  22544  mdetf  22551  mdetdiaglem  22554  mdetrlin  22558  mdetrsca  22559  mdetralt  22564  mdetunilem7  22574  mdetunilem9  22576  maducoeval2  22596  madutpos  22598  madugsum  22599  madurid  22600  cramerimplem1  22639  m2pmfzmap  22703  decpmatval  22721  pmatcollpw3lem  22739  pmatcollpw3fi1lem1  22742  pmatcollpw3fi1lem2  22743  pm2mp  22781  chfacfisf  22810  chfacfisfcpmat  22811  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  chfacfpmmulgsum2  22821  cayhamlem1  22822  cpmadugsumlemF  22832  cpmadugsumfi  22833  cayhamlem2  22840  chcoeffeqlem  22841  cayleyhamilton1  22848  pnrmopn  23299  xkoptsub  23610  xkopt  23611  tmdgsum  24051  imasdsf1olem  24329  rrxnm  25359  rrxds  25361  rrxf  25369  rrxmvallem  25372  rrxbasefi  25378  rrxdsfi  25379  ehlbase  25383  ovolscalem2  25483  uniioombl  25558  tdeglem2  26034  plypf1  26185  ulmclm  26364  ulmcaulem  26371  ulmcau  26372  ulmss  26374  ulmbdd  26375  ulmcn  26376  ulmdvlem1  26377  ulmdvlem2  26378  ulmdvlem3  26379  mtest  26381  mtestbdd  26382  mbfulm  26383  iblulm  26384  itgulm  26385  itgulm2  26386  adjval2  31978  fmptco1f1o  32722  fcobijfs  32810  fcobijfs2  32811  resf1o  32819  fpwrelmap  32822  elrspunidl  33520  elrspunsn  33521  1arithidomlem2  33628  1arithidom  33629  fply1  33650  psrbasfsupp  33704  ply1degltdimlem  33799  fedgmullem1  33806  fedgmul  33808  extdg1id  33843  smatrcl  33973  mbfmf  34431  elmbfmvol2  34444  eulerpartlemelr  34534  eulerpartlemf  34547  eulerpartlemt  34548  eulerpartgbij  34549  eulerpartlemgu  34554  eulerpartlemgh  34555  eulerpartlemgf  34556  eulerpartlemgs2  34557  reprf  34789  reprsuc  34792  vtsprod  34816  circlemethhgt  34820  tgoldbachgtd  34839  satfv1lem  35575  satfvel  35625  satefvfmla0  35631  satefvfmla1  35638  prv1n  35644  mrsubff1  35727  mrsub0  35729  mrsubf  35730  mrsubccat  35731  mrsubcn  35732  msubrn  35742  msubff  35743  msubf  35745  msubff1  35769  mclsind  35783  uncf  37844  curunc  37847  unccur  37848  matunitlindflem1  37861  matunitlindflem2  37862  poimirlem4  37869  poimirlem5  37870  poimirlem6  37871  poimirlem7  37872  poimirlem8  37873  poimirlem10  37875  poimirlem11  37876  poimirlem12  37877  poimirlem16  37881  poimirlem17  37882  poimirlem18  37883  poimirlem19  37884  poimirlem20  37885  poimirlem21  37886  poimirlem22  37887  poimirlem25  37890  poimirlem26  37891  poimirlem27  37892  poimirlem29  37894  poimirlem30  37895  poimirlem31  37896  poimirlem32  37897  poimir  37898  broucube  37899  mblfinlem3  37904  mblfinlem4  37905  ismblfin  37906  rrnmet  38074  rrndstprj1  38075  rrndstprj2  38076  rrncmslem  38077  rrnequiv  38080  aks6d1c2lem4  42491  mapcod  42607  evlselv  42939  fsuppind  42942  mhphf  42949  mapco2g  43065  mapfzcons1  43068  mapfzcons2  43070  mzpcompact2lem  43102  eldiophb  43108  elmapresaunres2  43122  eq0rabdioph  43127  rexrabdioph  43145  eldioph4b  43162  diophren  43164  rmydioph  43365  rmxdioph  43367  expdiophlem2  43373  expdioph  43374  pw2f1o2val2  43391  wepwsolem  43393  pwfi2f1o  43447  ofoafo  43707  ofoaid1  43709  ofoaid2  43710  ofoaass  43711  ofoacom  43712  rfovcnvf1od  44354  rfovcnvfvd  44357  fsovrfovd  44359  fsovcnvlem  44363  ntrk0kbimka  44389  neik0pk1imk0  44397  ntrclsfveq1  44410  ntrclsfveq2  44411  ntrclsfveq  44412  ntrclsss  44413  ntrclsiso  44417  ntrclsk2  44418  ntrclskb  44419  ntrclsk3  44420  ntrclsk13  44421  ntrclsk4  44422  ntrneifv3  44432  ntrneineine0lem  44433  ntrneineine1lem  44434  ntrneifv4  44435  ntrneiel2  44436  ntrneicls00  44439  ntrneicls11  44440  ntrneiiso  44441  ntrneik2  44442  ntrneikb  44444  ntrneixb  44445  ntrneik3  44446  ntrneix3  44447  ntrneik13  44448  ntrneix13  44449  ntrneik4w  44450  ntrneik4  44451  clsneifv3  44460  clsneifv4  44461  neicvgfv  44471  k0004ss2  44502  k0004val0  44504  mnringbasefd  44568  mnugrud  44634  mapss2  45557  difmap  45559  inmap  45561  difmapsn  45564  ssmapsn  45568  mccllem  45951  dvnprodlem1  46298  dvnprodlem2  46299  fourierdlem11  46470  fourierdlem12  46471  fourierdlem13  46472  fourierdlem14  46473  fourierdlem34  46493  fourierdlem41  46500  fourierdlem48  46506  fourierdlem49  46507  fourierdlem54  46512  fourierdlem63  46521  fourierdlem64  46522  fourierdlem65  46523  fourierdlem69  46527  fourierdlem72  46530  fourierdlem74  46532  fourierdlem75  46533  fourierdlem79  46537  fourierdlem85  46543  fourierdlem88  46546  fourierdlem89  46547  fourierdlem90  46548  fourierdlem91  46549  fourierdlem92  46550  fourierdlem94  46552  fourierdlem97  46555  fourierdlem103  46561  fourierdlem104  46562  fourierdlem111  46569  fourierdlem113  46571  etransclem24  46610  etransclem26  46612  etransclem27  46613  etransclem28  46614  etransclem31  46617  etransclem32  46618  etransclem33  46619  etransclem34  46620  etransclem35  46621  etransclem37  46623  etransclem38  46624  rrxtopnfi  46639  rrndistlt  46642  qndenserrnbllem  46646  rrxsnicc  46652  ioorrnopnlem  46656  subsaliuncl  46710  hoicvr  46900  ovnprodcl  46906  ovnsupge0  46909  ovnlecvr  46910  ovncvrrp  46916  ovn0lem  46917  ovnsubaddlem1  46922  sge0hsphoire  46941  hoidmv1le  46946  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  hoidmvlelem4  46950  hoidmvlelem5  46951  hoidmvle  46952  ovnhoilem2  46954  ovnlecvr2  46962  ovncvr2  46963  hoiqssbllem1  46974  hoiqssbllem2  46975  hoiqssbllem3  46976  hspmbllem2  46979  opnvonmbllem2  46985  ovolval2lem  46995  ovolval2  46996  ovolval3  46999  ovolval4lem2  47002  ovolval5lem3  47006  ovnovollem1  47008  ovnovollem2  47009  vonvolmbllem  47012  vonvolmbl2  47015  vonvol2  47016  snvonmbl  47038  vonsn  47043  iccpartxr  47773  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  intop  48557  assintop  48563  isassintop  48564  ofaddmndmap  48697  rmsupp0  48722  domnmsuppn0  48723  rmsuppss  48724  scmsuppss  48725  gsumlsscl  48734  lincfsuppcl  48767  linccl  48768  lcosn0  48774  lincdifsn  48778  lincsum  48783  lincscm  48784  lincscmcl  48786  islinindfis  48803  lincext1  48808  lincext2  48809  lincext3  48810  lindslinindimp2lem1  48812  lindslinindimp2lem2  48813  lindslinindimp2lem4  48815  lindslinindsimp2lem5  48816  snlindsntor  48825  lincresunitlem2  48830  lincresunit3lem1  48833  lincresunit3lem2  48834  lincresunit3  48835  lincreslvec3  48836  isldepslvec2  48839  zlmodzxzldeplem2  48855  zlmodzxzldeplem3  48856  ldepsnlinclem1  48859  ldepsnlinclem2  48860  1arymaptf1  48996  1arymaptfo  48997  2arympt  49003  2arymaptf1  49007  2arymaptfo  49008  prelrrx2b  49068  eenglngeehlnmlem1  49091  eenglngeehlnmlem2  49092  aacllem  50154